Trees over Infinite Structures and Path Logics with Synchronization

Alex Spelten
(RWTH Aachen University)
Wolfgang Thomas
(RWTH Aachen University)
Sarah Winter
(RWTH Aachen University)

We provide decidability and undecidability results on the model-checking problem for infinite tree structures. These tree structures are built from sequences of elements of infinite relational structures. More precisely, we deal with the tree iteration of a relational structure M in the sense of Shelah-Stupp. In contrast to classical results where model-checking is shown decidable for MSO-logic, we show decidability of the tree model-checking problem for logics that allow only path quantifiers and chain quantifiers (where chains are subsets of paths), as they appear in branching time logics; however, at the same time the tree is enriched by the equal-level relation (which holds between vertices u, v if they are on the same tree level). We separate cleanly the tree logic from the logic used for expressing properties of the underlying structure M. We illustrate the scope of the decidability results by showing that two slight extensions of the framework lead to undecidability. In particular, this applies to the (stronger) tree iteration in the sense of Muchnik-Walukiewicz.

In Fang Yu and Chao Wang: Proceedings 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011), Taipei, Taiwan, 10th October 2011, Electronic Proceedings in Theoretical Computer Science 73, pp. 20–34.
Published: 11th November 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: