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 inﬁnite tree structures. These tree structures are built from sequences of elements of inﬁnite 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 quantiﬁers and chain quantiﬁers (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. |

Published: 11th November 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.73.5 | bibtex | |

Comments and questions to: eptcs@eptcs.org |

For website issues: webmaster@eptcs.org |