Document Open Access Logo

Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2020.141.pdf
  • Filesize: 0.6 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
Keywords
  • PDA
  • Bisimulation
  • Equivalence checking

Metrics

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.

Cite As Get BibTex

Wenbo Zhang, Qiang Yin, Huan Long, and Xian Xu. Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 141:1-141:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ICALP.2020.141

Author Details

Wenbo Zhang
  • BASICS, Shanghai Jiao Tong University, Shanghai, China
Qiang Yin
  • Alibaba Group, Shanghai, China
Huan Long
  • BASICS, Shanghai Jiao Tong University, Shanghai, China
Xian Xu
  • East China University of Science and Technology, Shanghai, China

Acknowledgements

This work is supported by NSF of China (61772336, 61872142, 61572318). The authors are grateful to Yuxi Fu for insightful discussions on this topic and support. We also thank the anonymous reviewers for their helpful comments and suggestions.

References

  1. Jos CM Baeten, Jan A Bergstra, and Jan Willem Klop. Decidability of bisimulation equivalence for process generating context-free languages. Journal of the ACM, 40(3):653-682, 1993. URL: https://doi.org/10.1145/174130.174141.
  2. Michael Benedikt, Stefan Göller, Stefan Kiefer, and Andrzej S Murawski. Bisimilarity of pushdown automata is nonelementary. In Proc. LICS '13, pages 488-498. IEEE, 2013. URL: https://doi.org/10.1109/LICS.2013.55.
  3. Didier Caucal. Bisimulation of context-free grammars and of pushdown automata. Modal Logic and Process Algebra, 53:85-106, 1995. Google Scholar
  4. Bruno Courcelle. Recursive applicative program schemes. In Formal Models and Semantics, pages 459-492. Elsevier, 1990. URL: https://doi.org/10.1016/B978-0-444-88074-1.50014-7.
  5. Seymour Ginsburg and Sheila Greibach. Deterministic context free languages. Information and Control, 9(6):620-648, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80019-0.
  6. J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley Publishing Company, 1979. Google Scholar
  7. Petr Jančar. Decidability of DPDA Language Equivalence via First-Order Grammars. In Proc. LICS '12, pages 415-424. IEEE, 2012. URL: https://doi.org/10.1109/LICS.2012.51.
  8. Petr Jančar. Bisimulation Equivalence of First-Order Grammars. In Proc. ICALP '14, LNCS, pages 232-243. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_20.
  9. Petr Jančar. Equivalences of pushdown systems are hard. In Proc. FoSSaCS '14, pages 1-28. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_1.
  10. Petr Jančar and Sylvain Schmitz. Bisimulation equivalence of first-order grammars is ACKERMANN-complete. In Proc. LICS '19, pages 1-12. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785848.
  11. Petr Jančar and Jivří Srba. Undecidability of bisimilarity by Defender’s forcing. Journal of the ACM (JACM), 55(1):5, 2008. URL: https://doi.org/10.1145/1326554.1326559.
  12. Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters, 113(4):101-106, 2013. URL: https://doi.org/10.1016/j.ipl.2012.12.004.
  13. Antonín Kučera and Petr Jančar. Equivalence-checking on infinite-state systems: Techniques and results. Theory and Practice of Logic Programming, 6(201), 2006. URL: https://doi.org/10.1017/S1471068406002651.
  14. Antonín Kučera and Richard Mayr. On the complexity of checking semantic equivalences between pushdown processes and finite-state processes. Information and Computation, 208(7):772-796, 2010. URL: https://doi.org/10.1016/j.ic.2010.01.003.
  15. Robin Milner. Communication and concurrency, volume 84. Prentice-Hall, Inc., 1989. Google Scholar
  16. Michio Oyamaguchi. The equivalence problem for real-time DPDAs. Journal of the ACM (JACM), 34(3):731-760, 1987. URL: https://doi.org/10.1145/28869.28881.
  17. V Yu Romanovskii. The equivalence problem for real-time deterministic pushdown automata. Cybernetics, 22(2):162-175, 1986. URL: https://doi.org/10.1007/BF01074776.
  18. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory (TOCT), 8(1):3, 2016. URL: https://doi.org/10.1145/2858784.
  19. Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Habilitation thesis, École Normale Supérieure Paris-Saclay, 2017. Google Scholar
  20. Sylvain Schmitz. The parametric complexity of lossy counter machines. In Proc. ICALP '19, volume 132, pages 129:1-129:15. LZI, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.129.
  21. Philippe Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In Proc. MFCS '10, pages 616-628. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15155-2_54.
  22. Géraud Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proc. FOCS '98, pages 120-129. IEEE, 1998. URL: https://doi.org/10.1109/SFCS.1998.743435.
  23. Géraud Sénizergues. L(A)=L(B)? Decidability results from complete formal systems. Theoretical Computer Science, 251(1-2):1-166, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00285-1.
  24. Géraud Sénizergues. The bisimulation problem for equational graphs of finite out-degree. SIAM Journal on Computing, 34(5):1025-1106, 2005. URL: https://doi.org/10.1137/S0097539700377256.
  25. Colin Stirling. Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 195(2):113-131, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00216-8.
  26. Colin Stirling. Decidability of bisimulation equivalence for pushdown processes. Technical report, University of Edinburgh, 2000. Google Scholar
  27. Colin Stirling. Decidability of DPDA equivalence. Theor. Comput. Sci., 255(1-2):1-31, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00389-3.
  28. Colin Stirling. Deciding DPDA equivalence is primitive recursive. In Proc. ICALP '02, pages 821-832. Springer, 2002. URL: https://doi.org/10.1007/3-540-45465-9_70.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact