The parametric complexity of bisimulation equivalence of normed pushdown automata

Abstract

Deciding bisimulation equivalence of two normed pushdown automata is one of the most fundamental problems in formal verification. The problem is proven to be ACKERMANN-complete recently. Both the upper bound and the lower bound results indicate that the number of control states is an important parameter. In this paper, we study the parametric complexity of this problem. We refine previous results in two aspects. First, we prove that the bisimulation equivalence of normed PDA with two states is EXPTIME-hard. Second, we prove that the bisimulation equivalence of normed PDA with d states is in {\mathbf{F}}_{d+3}, which improves the best known upper bound {\mathbf{F}}_{d+4} of this problem.

Graphical abstract

Keywords

PDA / bisimulation / equivalence checking

References

[1] Park D. Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI Conference, Lecture Notes in Computer Science. 1981, 167–183

[2] Milner R. Communication and concurrency. 1st ed. New Jersey: Prentice-Hall, Inc., 1989

[3] Van Glabbeek R J , Weijland W P . Branching time and abstraction in bisimulation semantics. Journal of the ACM (JACM), 1996, 43( 3): 555– 600

[4] Hopcroft J, Ullman J. Introduction to Automata Theory, Languages and Computation. 1st ed. New York: Addison-Wesley Publishing Company, 1979

[5] Ginsburg S , Greibach S . Deterministic context free languages. Information and Control, 1966, 9( 6): 620– 648

[6] Sénizergues G . L(A)=L(B)? Decidability results from complete formal systems. Theoretical Computer Science, 2001, 251( 1−2): 1– 166

[7] Stirling C. Deciding DPDA equivalence is primitive recursive. In: Proceedings of the 29th International Colloquium on Automata, Languages, and Programming. 2002, 821–832

[8] Jančar P. Equivalences of pushdown systems are hard. In: Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures. 2014, 1–28

[9] Sénizergues G. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In: Proceedings of the 39th Annual Symposium on Foundations of Computer Science. 1998, 120–129

[10] Sénizergues G . The bisimulation problem for equational graphs of finite out-degree. SIAM Journal on Computing, 2005, 34( 5): 1025– 1106

[11] Srba J. Undecidability of weak bisimilarity for pushdown processes. In: Proceedings of International Conference on Concurrency Theory. 2002, 579– 594

[12] Yin Q, Fu Y, He C, Huang M, Tao X. Branching bisimilarity checking for PRS. In: Proceedings of International Colloquium on Automata, Languages, and Programming. 2014, 363– 374

[13] Jančar P, Schmitz S. Bisimulation equivalence of first-order grammars is Ackermann-complete. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2019, 1–12

[14] Jančar P. Decidability of DPDA language equivalence via first-order grammars. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science. 2012, 415–424

[15] Kučera A , Mayr R . On the complexity of checking semantic equivalences between pushdown processes and finite-state processes. Information and Computation, 2010, 208( 7): 772– 796

[16] Benedikt M, Göller S, Kiefer S, Murawski A S. Bisimilarity of pushdown automata is nonelementary. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science. 2013, 488–498

[17] Zhang W, Yin Q, Long H, Xu X. Bisimulation equivalence of pushdown automata is Ackermann-complete. In: Proceedings of 47th International Colloquium on Automata, Languages, and Programming. 2020, 141: 1– 14

[18] Kiefer S . BPA bisimilarity is EXPTIME-hard. Information Processing Letters, 2013, 113( 4): 101– 106

[19] Burkart O, Caucal D, Steffen B. An elementary bisimulation decision procedure for arbitrary context-free processes. In: Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science. 1995, 423–433

[20] Jančar P. Bisimilarity on basic process algebra is in 2-Exptime (an explicit proof). preprint arXiv: 1207.2479, 1207

[21] Böhm S , Göller S , Jančar P . Bisimulation equivalence and regularity for real-time one-counter automata. Journal of Computer and System Sciences, 2014, 80( 4): 720– 743

[22] Hirshfeld Y , Jerrum M , Moller F . A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science, 1996, 158( 1−2): 143– 159

[23] Balcázar J , Gabarro J , Santha M . Deciding bisimilarity is P-complete. Formal aspects of computing, 1992, 4( 1): 638– 648

[24] Schmitz S . Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory (TOCT), 2016, 8( 1): 3–

[25] Thomas W. On the ehrenfeucht-fraïssé game in theoretical computer science. In: Proceedings of Colloquium on Trees in Algebra and Programming. 1993, 559– 568

[26] Jančar P , Srba J . Undecidability of bisimilarity by Defender’s forcing. Journal of the ACM (JACM), 2008, 55( 1): 5–

[27] Srba J. Applications of the existential quantification technique. In: Proceedings of the 4th International Workshop on Verification of Infinite-State Systems (INFINITY02). 2002, 151– 152

[28] Srba J . Strong bisimilarity of simple process algebras: Complexity lower bounds. Acta Informatica, 2003, 39( 6−7): 469– 499

[29] Stirling C . Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 1998, 195( 2): 113– 131

[30] Stirling C. Decidability of bisimulation equivalence for normed pushdown processes. In: Proceedings of the 7th International Conference on Concurrency Theory. 1996, 217–232

[31] Jančar P. Equivalence of pushdown automata via first-order grammars. arXiv: 1812.03518, 2018

[32] Schmitz S. Complexity bounds for ordinal-based termination. In: Proceedings of the 8th International Workshop on Reachability Problems. 2014, 1–19

RIGHTS & PERMISSIONS

Higher Education Press