|
Inference
of
Extended
Finite
State
Machines
Title: |
Inference of Extended Finite State Machines |
Authors:
|
Michael Foster (jmafoster1 /at/ sheffield /dot/ ac /dot/ uk),
Achim D. Brucker,
Ramsay G. Taylor (r /dot/ g /dot/ taylor /at/ sheffield /dot/ ac /dot/ uk) and
John Derrick (j /dot/ derrick /at/ sheffield /dot/ ac /dot/ uk)
|
Submission date: |
2020-09-07 |
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. |
BibTeX: |
@article{Extended_Finite_State_Machine_Inference-AFP,
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,
note = {\url{https://isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Extended_Finite_State_Machines |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|