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 P_i
• O is a set of output symbols with symbolic parameters, where for each output symbol o we have a set of symbolic output parameters P_o
• V is set of n symbolic statevars v_i ... v_n
• D_V is an n-dimensional linear space D₁ x ... x D_n for the valuation of the statevars V,
• D_i is an m-dimensional linear space D₁ x ... x D_m for the valuation of the set of symbolic input parameters P_i of input i,
• F is a set of enabling functions f_k : D_i x D_V -> {0,1},
• U is a set of update functions u_k : D_i x D_V -> D_V for updating the valuation of the statevars V,
• P is a set of output functions p_k : D_i x D_V -> D_p, where D_p 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 p_k : D_V -> D_p, where D_p 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.