The Limits of Decidability for First Order Logic on CPDA Graphs

Christopher H. Broadbent
Higher-order pushdown automata (n-PDA) are abstract machines equipped with a nested 'stack of stacks of stacks'. Collapsible pushdown automata (n-CPDA) extend these devices by adding `links' 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...