A Formal Model of Extended Finite State Machines

By Michael Foster, Achim D. Brucker, Ramsay G. Taylor, and John Derrick.

In this AFP entry, we provide a formalisation of extended finite state machines (EFSMs) where models are represented as finite sets of transitions between states. EFSMs execute traces to produce observable outputs. We also define various simulation and equality metrics for EFSMs in terms of traces and prove their strengths in relation to each other. Another key contribution is a framework of function definitions such that LTL properties can be phrased over EFSMs. Finally, we provide a simple example case study in the form of a drinks machine.

Please cite this work as follows:
M. Foster, A. D. Brucker, R. G. Taylor, and J. Derrick, “A formal model of extended finite state machines,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Extended_Finite_State_Machines.html, Formal proof development. Author copy: https://logicalhacking.com/publications/foster.ea-efsm-2020/

BibTeX
@Article{ foster.ea:efsm:2020,
  author    = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and
               John Derrick},
  title     = {A Formal Model of Extended Finite State Machines},
  journal   = {Archive of Formal Proofs},
  month     = {sep},
  year      = {2020},
  date      = {2020-09-07},
  note      = {\url{https://www.isa-afp.org/entries/Extended_Finite_State_Machines.html},
               Formal proof development. 
               Author copy: \url{https://logicalhacking.com/publications/foster.ea-efsm-2020/}},
  issn      = {2150-914x},
  abstract  = {In this AFP entry, we provide a formalisation of extended
               finite state machines (EFSMs) where models are represented as
               finite sets of transitions between states. EFSMs execute
               traces to produce observable outputs. We also define various
               simulation and equality metrics for EFSMs in terms of traces
               and prove their strengths in relation to each other. Another
               key contribution is a framework of function definitions such
               that LTL properties can be phrased over EFSMs. Finally, we
               provide a simple example case study in the form of a drinks
               machine.},
  filelabel = {Outline},
  file      = {download/2020/foster.ea-efsm-outline-2020.pdf},
  areas     = {formal methods, software engineering},
  pdf       = {https://logicalhacking.com/publications/foster.ea-efsm-2020/foster.ea-efsm-2020.pdf},
}