Nested Pushdown Trees are unfoldings of pushdown graphs with an additional jump-relation. These graphs are closely related to collapsible pushdown graphs. They enjoy decidable μ-calculus model checking while monadic second-order logic is undecidable on this class. We show that nested pushdown trees are tree-automatic structures, whence first-order model checking is decidable. Furthermore, we prove that it is in 2-EXPSPACE using pumping arguments on runs of pushdown systems. For these arguments we also develop a Gaifman style argument for graphs of small diameter. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Kartzow, A. (2009). FO model checking on nested pushdown trees. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5734 LNCS, pp. 451–463). https://doi.org/10.1007/978-3-642-03816-7_39
Mendeley helps you to discover research relevant for your work.