The Limits of Decidability for First Order Logic on CPDA Graphs

Higher-order pushdown automata (n-PDA) are abstract machines equipped with a nested \u27stack of stacks of stacks\u27. Collapsible pushdown automata (n-CPDA) extend these devices by adding `links\u27 to the stack and are equi-expressive for tree generation with simply typed lambda-Y terms. Whilst the configuration graphs of HOPDA are well understood, relatively little is known about the CPDA graphs. The order-2 CPDA graphs already have undecidable MSO theories but it was only recently shown by Kartzow [Kartzow 2010] that first-order logic is decidable at the second level. In this paper we show the surprising result that first-order logic ceases to be decidable at order-3 and above. We delimit the fragments of the decision problem to which our undecidability result applies in terms of quantifer alternation and the orders of CPDA links used. Additionally we exhibit a natural sub-hierarchy enjoying limited decidability