Inference of Extended Finite State Machines

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

In this AFP entry, we provide a formal implementation of a state-merging technique to infer extended finite state machines (EFSMs), complete with output and update functions, from black-box traces. In particular, we define the subsumption in context relation as a means of determining whether one transition is able to account for the behaviour of another. Building on this, we define the direct subsumption relation, which lifts the subsumption in context relation to EFSM level such that we can use it to determine whether it is safe to merge a given pair of transitions. Key proofs include the conditions necessary for subsumption to occur and that subsumption and direct subsumption are preorder relations. We also provide a number of different heuristics which can be used to abstract away concrete values into registers so that more states and transitions can be merged and provide proofs of the various conditions which must hold for these abstractions to subsume their ungeneralised counterparts. A Code Generator setup to create executable Scala code is also defined.

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

BibTeX
@Article{ foster.ea:efsm-inference:2020,
  author    = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and
               John Derrick},
  title     = {Inference 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_Machine_Inference.html},
               Formal proof development. 
               Author copy: \url{https://logicalhacking.com/publications/foster.ea-efsm-inference-2020/}},
  issn      = {2150-914x},
  abstract  = {In this AFP entry, we provide a formal implementation of a
               state-merging technique to infer extended finite state
               machines (EFSMs), complete with output and update functions,
               from black-box traces. In particular, we define the
               subsumption in context relation as a means of determining
               whether one transition is able to account for the behaviour of
               another. Building on this, we define the direct subsumption
               relation, which lifts the subsumption in context relation to
               EFSM level such that we can use it to determine whether it is
               safe to merge a given pair of transitions. Key proofs include
               the conditions necessary for subsumption to occur and that
               subsumption and direct subsumption are preorder relations. We
               also provide a number of different heuristics which can be
               used to abstract away concrete values into registers so that
               more states and transitions can be merged and provide proofs
               of the various conditions which must hold for these
               abstractions to subsume their ungeneralised counterparts. A
               Code Generator setup to create executable Scala code is also
               defined.},
  filelabel = {Outline},
  file      = {download/2020/foster.ea-efsm-inference-outline-2020.pdf},
  areas     = {formal methods, software engineering},
  pdf       = {https://logicalhacking.com/publications/foster.ea-efsm-inference-2020/foster.ea-efsm-inference-2020.pdf},
}