On Bisimilarity of Higher-Order Pushdown Automata: Undecidability at Order Two

Authors Christopher Broadbent, Stefan Göller

Thumbnail PDF


  • Filesize: 0.51 MB
  • 13 pages

Document Identifiers

Author Details

Christopher Broadbent
Stefan Göller

Cite AsGet BibTex

Christopher Broadbent and Stefan Göller. On Bisimilarity of Higher-Order Pushdown Automata: Undecidability at Order Two. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 160-172, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


We show that bisimulation equivalence of order-two pushdown automata is undecidable. Moreover, we study the lower order problem of higher-order pushdown automata, which asks, given an order-k pushdown automaton and some k'<k, to determine if there exists a reachable configuration that is bisimilar to some order-k' pushdown automaton. We show that the lower order problem is undecidable for each k >= 2 even when the input k-PDA is deterministic and real-time.
  • Bisimulation equivalence
  • Higher-order pushdown automata


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail