This paper presents a mechanical technique which allows behavioural equivalence proof between (nondeterministic) finite-state machines (FSMs). Given a pair of FSMs which are recursively described in the syntax of a process algebra, a third FSM which represents the concurrent behaviour of the two original FSMs is constructed. An algorithm is engineered for comparing the two FSMs against this third concurrent FSM. A self-evident proof of the equivalence between the FSMs will be produced; if the two FSMs are not equivalent, a sequnce of events will be returned which distinguishes between them.
CITATION STYLE
Mao, W., & Milne, G. J. (1992). An automated proof technique for finite-state machine equivalence. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 575 LNCS, pp. 233–243). Springer Verlag. https://doi.org/10.1007/3-540-55179-4_23
Mendeley helps you to discover research relevant for your work.