We study languages of nested trees-structures obtained by augmenting trees with sets of nested jump-edges. These graphs can naturally model branching behaviors of pushdown programs, so that the problem of branching-time software model checking may be phrased as a membership question for such languages. We define finite-state automata accepting such languages-these automata can pass states along jumpedges as well as tree edges. We find that the model-checking problem for these automata on pushdown systems is EXPTIME-complete, and that their alternating versions are expressively equivalent to NT-μ, a recently proposed temporal logic for nested trees that can express a variety of branching-time, "context-free" requirements. We also show that monadic second order logic (MSO) cannot exploit the structure: MSO on nested trees is too strong in the sense that it has an undecidable model checking problem, and seems too weak to capture NT-μ. © Springer-Vorlag Berlin Heidelberg 2006.
CITATION STYLE
Alur, R., Chaudhuri, S., & Madhusudan, P. (2006). Languages of nested trees. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4144 LNCS, pp. 329–342). Springer Verlag. https://doi.org/10.1007/11817963_31
Mendeley helps you to discover research relevant for your work.