The Limits of Decidability for First Order Logic on CPDA Graphs

Author Christopher H. Broadbent

Thumbnail PDF


  • Filesize: 0.68 MB
  • 12 pages

Document Identifiers

Author Details

Christopher H. Broadbent

Cite AsGet BibTex

Christopher H. Broadbent. The Limits of Decidability for First Order Logic on CPDA Graphs. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 589-600, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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 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.
  • Collapsible Pushdown Automata
  • First Order Logic
  • Logical Reflection


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads