2026-08-15T00:44:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12548 2024-03-06T10:50:25Z ddc:004 open_access

Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete Zhang, Wenbo Yin, Qiang Long, Huan Xu, Xian PDA Bisimulation Equivalence checking Deciding bisimulation equivalence of two pushdown automata is one of the most fundamental problems in formal verification. Though Sénizergues established decidability of this problem in 1998, it has taken a long time to understand its complexity: the problem was proven to be non-elementary in 2013, and only recently, Jančar and Schmitz showed that it has an Ackermann upper bound. We improve the lower bound to Ackermann-hard, and thus close the complexity gap. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Wenbo Zhang and Qiang Yin and Huan Long and Xian Xu 2020 Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2020.141 urn:nbn:de:0030-drops-125482 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.141 eng https://creativecommons.org/licenses/by/3.0/legalcode