Abstract
The paper addresses the problem of solving an equation formulated in terms of the input/output finite state machine model. The relation used in equations is either FSM equivalence or reduction, i.e. trace inclusion. The composition operator corresponds to asynchronous communications between nondeterministic input/output machines. These types of FSM equations are called asynchronous. A procedure for determining the largest potential solution to a given asynchronous equation is proposed. To verify whether or not the largest potential solution satisfies the equation, the absence of livelocks needs to be established. A solution to the livelock problem is also suggested.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35394-4_29
Chapter PDF
References
A. Aziz, F. Balarin, R. K. Brayton, M. D. DiBenedetto, and A. Saldanha, Supervisory Control of Finite State Machines, Proceedings of the 7th International Conference, CAV’95, Belgium, pp. 279–292, 1995.
F. Cecseg, Products of Automata, Monographs in Theoretical Computer Science. Springer Verlag, 1986.
S. C. Cheung and J. Kramer. Context constraints for compositional reachability analysis, ACM Trans. on Software Engineering and Methodology, Vol. 5, N 4, 1996, pp. 334–377.
M. Damiani, Nondeterministic finite state machines and sequential don’t cares, Proceedings of the Euro Design and Test Conference, 1994.
L. Heerink and E. Brinksma, Validation in context, Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing, and Verification, Chapman & Hall (1995), pp 221–236.
J. E. Hoperoft and J. D. Ullman (1979) Introduction to automata theory, languages, and computation, Addison-Wesley, New York.
J. Kim and M. Newborn. The simplification of sequential machines with input restrictions, IEEE Trans. on Computers, C-20, pp. 1440–1443, 1972.
K. Larsen and L. Xinxin, Compositionality through an operational semantics of contexts, Lecture Notes in Computer Science, Vol 443, 1990.
B. Lin, G. de Jong, and T. Kolks, Hierarchical optimization of asynchronous circuits, Proceedings of the 32nd Design Automation Conference, 1995, pp. 712–717.
Lee93] D. Lee, K. Sabnani, D. Krispot, S. Paul, and M. Uyar, Conformance testing of protocols specified as communicating fsms,INFOCOM’93.
P. Merlin and G. v. Bochmann, On the Construction of Submodule Specifications and Communication Protocols, ACM Trans. on Programming Languages and Systems, Vol. 5, No. 1, Jan. 1983, pp. 1–25.
H. Qin and P. Lewis, Factorisation of Finite State Machines under Strong and Observational Equivalences, Journal of Formal Aspects of Computing, Vol. 3, July-Sept. 1991, pp. 284–307.
J. Parrow. Submodule construction as equation solving in ccs, Theoretical Computer Science, 68, pp. 175–202, 1989.
A. Petrenko, N. Yevtushenko, A. Lebedev, and A. Das, Nondeterministic state machines in protocol conformance testing, Proceedings of the IFIP Sixth International Workshop on Protocol Test Systems, pp. 363–378, 1993.
A. Petrenko, N. Yevtushenko, and R. Dssouli, Testing strategies for communicating FSMs, Proceedings of the 7th IWTCS, (1994) pp. 193–208.
A. Petrenko, N. Yevtushenko, G. v. Bochmann, and R. Dssouli. Testing in context: framework and test derivation, Computer Communications, Vol. 19, pp. 1236–1249, 1996.
J.-K. Rho, G. Hachtel, and F. Somentzi. Don’t care sequences and the optimization of interacting finite state machines, Proceedings of the IEEE Conference on Computer-Aided Design, Santa Clara, 1991, pp. 414–421.
P. H. Starke, Abstract automata, American Elsevier Publishing Company, Inc. New York, 1972.
Y. Watanabe, and R. K. Brayton. The maximal set of permissible behaviors for fsm networks, Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, pp. 316–320, 1993.
Y. Watanabe and R. K. Brayton. State minimization of pseudo nondeterministic FSMs, Proceedings of Euro Design and Test Conference, pp. 184–191, 1994.
N. Yevtushenko and A. Matrosova. On one approach to automata networks checking sequences construction, Automatic Control and Computer Sciences, Allerton Press, NY, Vol. 25, N 2, pp. 3–7, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Petrenko, A., Yevtushenko, N. (1998). Solving asynchronous equations. In: Budkowski, S., Cavalli, A., Najm, E. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. PSTV FORTE 1998 1998. IFIP — The International Federation for Information Processing, vol 6. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35394-4_15
Download citation
DOI: https://doi.org/10.1007/978-0-387-35394-4_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5262-5
Online ISBN: 978-0-387-35394-4
eBook Packages: Springer Book Archive