Trees over Infinite Structures and Path Logics with Synchronization

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 Shela...

Full description

Bibliographic Details
Main Authors: Alex Spelten, Wolfgang Thomas, Sarah Winter
Format: Article
Language:English
Published: Open Publishing Association 2011-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1111.3107v1