文章基本信息
- 标题：Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete
- 本地全文：下载
- 作者：Wenbo Zhang ; Qiang Yin ; Huan Long 等
- 期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
- 电子版ISSN：1868-8969
- 出版年度：2020
- 卷号：168
- 页码：141:1-141:14
- DOI：10.4230/LIPIcs.ICALP.2020.141
- 出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
- 摘要：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.
- 关键词：PDA; Bisimulation; Equivalence checking
