Computer Science – Logic in Computer Science
Scientific paper
2011-11-14
EPTCS 73, 2011, pp. 20-34
Computer Science
Logic in Computer Science
In Proceedings INFINITY 2011, arXiv:1111.2678
Scientific paper
10.4204/EPTCS.73.5
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.
Spelten Alex
Thomas Wolfgang
Winter Sarah
No associations
LandOfFree
Trees over Infinite Structures and Path Logics with Synchronization does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Trees over Infinite Structures and Path Logics with Synchronization, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Trees over Infinite Structures and Path Logics with Synchronization will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-216673