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
Go to the corresponding LIPIcs Volume Portal

Zhang, Wenbo ; Yin, Qiang ; Long, Huan ; Xu, Xian

Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete

LIPIcs-ICALP-2020-141.pdf (0.6 MB)


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

  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 =		{},
  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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI