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.
@InProceedings{broadbent_et_al:LIPIcs.FSTTCS.2012.160, author = {Broadbent, Christopher and G\"{o}ller, Stefan}, title = {{On Bisimilarity of Higher-Order Pushdown Automata: Undecidability at Order Two}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)}, pages = {160--172}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-47-7}, ISSN = {1868-8969}, year = {2012}, volume = {18}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.160}, URN = {urn:nbn:de:0030-drops-38583}, doi = {10.4230/LIPIcs.FSTTCS.2012.160}, annote = {Keywords: Bisimulation equivalence, Higher-order pushdown automata} }
Feedback for Dagstuhl Publishing