FO Model Checking on Nested Pushdown Trees

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.

• Type: Conference
• Year: 2009
• Where: MFCS
• Authors: Alexander Kartzow
• Keywords: MFCS 2009, Nested Pushdown Trees, Pushdown, Pushdown Graphs, Theoretical Computer Science