Abstract
We consider infinite graphs that are generated by ground tree (or term) rewriting systems. The vertices of these graphs are trees. Thus, with a finite tree automaton one can represent a regular set of vertices. It is shown that for a regular set T of vertices the set of vertices from where one can reach (respectively, infinitely often reach) the set T is again regular. Furthermore it is shown that the problems, given a tree t and a regular set T, whether all paths starting in t eventually (respectively, infinitely often) reach T, are undecidable. We then define a logic which is in some sense a maximal fragment of temporal logic with a decidable model-checking problem for the class of ground tree rewriting graphs.
Chapter PDF
Similar content being viewed by others
References
Achim Blumensath and Erich Grädel. Automatic structures. In Proceedings of LICS’ 00, pages 51–62. IEEE Computer Society Press, 2000.
Walter S. Brainerd. Tree generating regular systems. Information and Control, 14:217–231, 1969.
Didier Caucal. On infinite transition graphs having a decidable monadic theory. In Proceedings ICALP’ 96, volume 1099 of LNCS. Springer-Verlag, 1996.
J.L. Coquidé, M. Dauchet, R. Gilleron, and S. Vágvölgyi. Bottom-up tree pushdown automata: Classification and connection with rewrite systems. Theoretical Computer Science, 127(1):69–98, 1994.
J.L. Coquidé and R. Gilleron. Proofs and reachability problem for ground rewrite systems. In Aspects and Prospects of Theoretical Computer Science, volume 464 of LNCS, pages 120–129. Springer, 1990.
Max Dauchet, Thierry Heuillard, Pierre Lescanne, and Sophie Tison. Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems. Information and Computation, 88(2):187–201, October 1990.
Max Dauchet and Sophie Tison. The theory of ground rewrite systems is decidable. In Proceedings LICS’ 90, pages 242–248. IEEE Computer Society Press, 1990.
Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In Proceedings of CAV 2000, volume 1855 of LNCS, pages 232–247. Springer-Verlag, 2000.
Javier Esparza and Astrid Kiehn. On the model checking problem for branching time logics and Basic Parallel Processes. In Proceedings of CAV’ 95, volume 939 of LNCS, pages 353–366, 1995.
Orna Kupferman and Moshe Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In E. A. Emerson and A. P. Sistla, editors, Proceedings of CAV 2000, volume 1855 of LNCS. Springer-Verlag, 2000.
Richard Mayr. Process rewrite systems. Information and Computation, 156(1–2):264–286, 2000.
Christophe Morvan. On rational graphs. In Proceedings of FoSSaCS’ 99, volume 1784 of LNCS, pages 252–266. Springer, 1999.
David E. Muller and Paul E. Schupp. The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37:51–75, 1985.
Igor Walukiewicz. Pushdown processes: Games and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of CAV’ 96, volume 1102 of LNCS, pages 62–74. Springer-Verlag, July–August 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Löding, C. (2002). Model-Checking Infinite Systems Generated by Ground Tree Rewriting. In: Nielsen, M., Engberg, U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2002. Lecture Notes in Computer Science, vol 2303. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45931-6_20
Download citation
DOI: https://doi.org/10.1007/3-540-45931-6_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43366-8
Online ISBN: 978-3-540-45931-6
eBook Packages: Springer Book Archive