License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2020.141
URN: urn:nbn:de:0030-drops-125482
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12548/
Zhang, Wenbo ;
Yin, Qiang ;
Long, Huan ;
Xu, Xian
Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete
Abstract
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.
BibTeX - Entry
@InProceedings{zhang_et_al:LIPIcs:2020:12548,
author = {Wenbo Zhang and Qiang Yin and Huan Long and Xian Xu},
title = {{Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete}},
booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
pages = {141:1--141:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-138-2},
ISSN = {1868-8969},
year = {2020},
volume = {168},
editor = {Artur Czumaj and Anuj Dawar and Emanuela Merelli},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12548},
URN = {urn:nbn:de:0030-drops-125482},
doi = {10.4230/LIPIcs.ICALP.2020.141},
annote = {Keywords: PDA, Bisimulation, Equivalence checking}
}
|
Keywords: |
|
PDA, Bisimulation, Equivalence checking |
|
Collection: |
|
47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
29.06.2020 |
