print · source · login   

Extended Finite State Machine (EFSM)

In a conventional finite state machine (FSM) there are no data parameters in the inputs nor outputs. An EFSM adds data to an FSM where it needs to add statevars and several functions related to data:

  • enabling/guard functions : an expression over the input parameters and statevars to decide whether a transition is enabled
  • update functions : whenever a transition is taken the update function calculates new values for the statevars
  • output functions : whenever a transition is taken the output function calculates new values for the output parameters

Note: for every FSM like DFA,NFA,Moore,Mealy,IA,IOA we can make an EFSM variant with data.

Formal definition Mealy EFSM

Source: http://www.wikiwand.com/en/Extended_finite-state_machine extended with symbolic input and output parameters

A Mealy EFSM is a 8-tuple M = (I,O,S,V,F,U,P,T)

  • S is a set of symbolic states,
  • I is a set of input symbols with symbolic parameters, where for each input symbol i we have a set of symbolic input parameters Pi
  • O is a set of output symbols with symbolic parameters, where for each output symbol o we have a set of symbolic output parameters Po
  • V is set of n symbolic statevars vi ... vn
  • DV is an n-dimensional linear space D1 x ... x Dn for the valuation of the statevars V,
  • Di is an m-dimensional linear space D1 x ... x Dm for the valuation of the set of symbolic input parameters Pi of input i,
  • F is a set of enabling functions fk : Di x DV -> {0,1},
  • U is a set of update functions uk : Di x DV -> DV for updating the valuation of the statevars V,
  • P is a set of output functions pk : Di x DV -> Dp, where Dp is the lineair space of the output parameter
  • T is a transition relation T : S x F x I -> S x U x O x P,

The operational semantics of an Mealy EFSM is a Mealy machine in which the states are pairs of a symbolic state and a valuation of the state variables. A transition may fire for given input values and current state variables valuation if its guard (F) evaluates to true. In this case, a new valuation of the state variables is computed using the update part of the transition(U), and also new valuation of the output parameters is computed using the output part of the transition(P).

Formal definition Moore EFSM

A Moore EFSM is a Mealy EFSM with a change to the output function :

  • P is a set of output functions pk : DV -> Dp, where Dp is the lineair space of the output parameter

That is the output only depends on the current symbolic state and the calculation of the valuation of the output paramaters only from the valuation of the state variables.