Abstract
We propose here an algorithm enabling to represent, in a finite way, some infinite reachability graphs of communicating finite-state machines, by using a graph grammar. The model-checking algorithm presented in Burkart and Quemener (1996) uses that finite representation for verifying properties of the infinite graph. In way to obtain that finite representation, we use a result of Jéron and Jard (1993): it can be detected that some sequences of transitions are infinitely repeated. We show here that the transitions issued from states linked by such sequences are also infinitely repeated if they are repeated twice. We deduce a method for detecting patterns that compose the infinite reachability graph on study.
Chapter PDF
Similar content being viewed by others
References
Baeten, J.C.M., Bergstra, J.A. and Klop, J.W. (1987) Decidability of bisimulation equiv-alence for processes generating context-free languages. In PARLE’87, LNCS 259, pages 94–113. Springer.
Boigelot, B. and Godefroid, B. (1996) Symbolic verification of communication protocols with infinite state spaces using QDDs. In CAV’96, to appear in LNCS.
Bochmann, G. (1978) Finite state descriptions of communication protocols. Computer Networks, 2.
Burkart, O. and Quemener, Y.-M. (1996) Model-checking of infinite graphs defined by graph grammars. Publication interne 995, IRISA. Presented at Infinity’96. Accessible at http://www.irisa.fr/EXTERNE/bibli/pi/PI-995.html.
Burkart, O. and Steffen, B. (1992) Model-checking for context-free processes. In CON-CUR’92, LNCS 836, pages 123–137. Springer.
Brand, D. and Zafiropoulo, P. (1983) On communicating finite-state machines. Journal of the ACM, 2, pages 323–342.
Caucal, D. (1992) On the regular structure of prefix rewriting. Theoretical Computer Science, 106, pages 61–86.
Courcelle, B. (1990) Graph rewriting: an algebraic and logic approach. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 5, pages 193–242. Elsevier Science Publisher B.V.
ISO 9074 (1989}) Estelle: a formal description technique based on an extended state transition model. ISO TC97/SC21/WG6.
Hüttel, H. and Stirling, C. (1991) Actions speak louder than words: proving bisimilarity for context-free processes. In 6th Annual IEEE Symposium on Logic in Computer Science, pages 376–386. IEEE Computer Society Press.
Hungar, H. and Steffen, B. (1993) Local model-checking for context-free processes. In ICALP’93, LNCS 700, pages 593–605. Springer.
Jéron, T. and Jard, C. (1993) Testing for unboundedness of FIFO channels. Theoretical Computer Science, 113, pages 93–117.
Muller, D.E. and Schupp, P.E. The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37, pages 51–75.
Purushothaman Iyer, S. (1993) A note on model-checking context-free processes. In North American Process Algebra Workshop.
Quemener, Y.-M. and Jéron, T. (1995) Model-checking of infinite Kripke structures de-fined by graph grammars. In Corradini, A. and Montanari, U., editors, Segragra’95, ENTCS 2, pages 67–74. Elsevier Science B.V.
Quemener, Y.-M. and Jéron, T. (1996) Finitely representing infinite reachability graphs of CFSMs with graph grammars. Publication interne 994, IRISA. Long version of current paper. Accessible at: http://www.irisa.fr/EXTERNE/bibli/pi/PI-994.html.
CCITT Recommendation Z.100. (1988) Specification and description language SDL. Blue Book, Vol. X.1-X.5.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Quemener, Y.M., Jéron, T. (1996). Finitely Representing Infinite Reachability Graphs of CFSMs with Graph Grammars. In: Gotzhein, R., Bredereke, J. (eds) Formal Description Techniques IX. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35079-0_23
Download citation
DOI: https://doi.org/10.1007/978-0-387-35079-0_23
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2883-4
Online ISBN: 978-0-387-35079-0
eBook Packages: Springer Book Archive