Abstract
In this paper, a formal model of Extended Finite State Machines (EFSMs) is proposed and an approach to their analysis is suggested. The state of an EFSM is captured by its configuration. A class of EFSMs, called Modular Vector Addition Systems (MVAS), is defined and analyzed. Modular Vector Addition Systems cover a significant subset of models used in communication protocols and behavioral synthesis of hardware. For this class of EFSMs, an algorithm to compute the set of configurations reachable from an initial configuration is presented. This algorithm may also be used to compute the set of recurrent configurations. Knowledge of these sets is useful in verification, testing, and optimization of EFSM models. A compact representation of these sets and a simple test for membership for such representations are also presented.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
ESTELLE — A Formal Description Technique based on an Extended State Transition Model. ISO 9074.
M.H. Sherif and A.S. Krishnakumar: Performance Evaluation From Formal Specifications of Protocols: A Case Study with LAPD. Proc. of Globecomm'90.
A. Bouajjani, J.-C. Fernandez, and N. Halbwachs: Minimal Model Generation. Proc. of II Workshop on Computer-Aided Verification, DIMACS Series Vol 3, ACM-AMS, 1990, pp. 85–91.
A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel: Minimal State Graph Generation. IMAG Grenoble preprint, 1991.
D. Lee and M. Yannakakis: Online Minimization of Transition Systems. Proc. of 24th ACM Symposium on the Theory of Computing, May 1992, pp. 264–274.
K.-T. Cheng and A.S. Krishnakumar: Automatic Functional Test generation Using The Extended Finite State Machine Model. Proc. of DAC '93.
E.W. Mayr: An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput. 13(3), pp. 441–460.
B.M. Stewart: Theory of Numbers. The MacMillan Company, New York, 1962.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krishnakumar, A.S. (1993). Reachability and recurrence in Extended Finite State Machines: Modular Vector Addition Systems. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_10
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive