The parametric complexity of bisimulation equivalence of normed pushdown automata

doi:10.1007/s11704-021-0340-x

Front. Comput. Sci.

2022, Vol. 16

Issue (4) : 164405 https://doi.org/10.1007/s11704-021-0340-x

RESEARCH ARTICLE

The parametric complexity of bisimulation equivalence of normed pushdown automata

Wenbo ZHANG^1,²(

)

¹. College of Information Technology, Shanghai Ocean University, Shanghai 201306, China
². BASICS Lab, School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai 200240, China

Download: PDF(907 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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 $F d + 3$ , which improves the best known upper bound $F d + 4$ of this problem.

Keywords PDA bisimulation equivalence checking

Corresponding Author(s): Wenbo ZHANG

Just Accepted Date: 26 January 2021 Issue Date: 01 December 2021

Cite this article:

Wenbo ZHANG. The parametric complexity of bisimulation equivalence of normed pushdown automata[J]. Front. Comput. Sci., 2022, 16(4): 164405.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-021-0340-x
https://academic.hep.com.cn/fcs/EN/Y2022/V16/I4/164405

	nPDA	PDA
$d = 1$	P [22]	2EXPTIME [20]
$d = 1$	P-hard [23]	EXPTIME-hard [18]
$d = 2$	$F 5$	$F 6$ [13]
$d = 2$	EXPTIME-hard	EXPTIME-hard [18]
$d = 3$	$F 6$	$F 7$ [13]
$d = 3$	EXPTIME-hard	EXPTIME-hard [18]
$d ≥ 4$	$F d + 3$	$F d + 4$ [13]
$d ≥ 4$	$F d ? 1$ -hard [17]	$F d ? 1$ -hard [17]

Tab.1 The parametric complexity of bisimilarity problem for (n)PDA

Fig.1 Defender’s forcing

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	R J Van Glabbeek , W P Weijland . Branching time and abstraction in bisimulation semantics. Journal of the ACM (JACM), 1996, 43( 3): 555– 600
4	J Hopcroft, J Ullman. Introduction to Automata Theory, Languages and Computation. 1st ed. New York: Addison-Wesley Publishing Company, 1979
5	S Ginsburg , S Greibach . Deterministic context free languages. Information and Control, 1966, 9( 6): 620– 648
6	G Sénizergues . 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	G Sénizergues . The bisimulation problem for equational graphs of finite out-degree. SIAM Journal on Computing, 2005, 34( 5): 1025– 1106
11	J Srba. Undecidability of weak bisimilarity for pushdown processes. In: Proceedings of International Conference on Concurrency Theory. 2002, 579– 594
12	Q Yin, Y Fu, C He, M Huang, X Tao. 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	A Kučera , R Mayr . 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	W Zhang, Q Yin, H Long, X Xu. Bisimulation equivalence of pushdown automata is Ackermann-complete. In: Proceedings of 47th International Colloquium on Automata, Languages, and Programming. 2020, 141: 1– 14
18	S Kiefer . 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	P Jančar. Bisimilarity on basic process algebra is in 2-Exptime (an explicit proof). preprint arXiv: 1207.2479, 1207
21	S Böhm , S Göller , P Jančar . Bisimulation equivalence and regularity for real-time one-counter automata. Journal of Computer and System Sciences, 2014, 80( 4): 720– 743
22	Y Hirshfeld , M Jerrum , F Moller . A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science, 1996, 158( 1−2): 143– 159
23	J Balcázar , J Gabarro , M Santha . Deciding bisimilarity is P-complete. Formal aspects of computing, 1992, 4( 1): 638– 648
24	S Schmitz . Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory (TOCT), 2016, 8( 1): 3–
25	W Thomas. On the ehrenfeucht-fraïssé game in theoretical computer science. In: Proceedings of Colloquium on Trees in Algebra and Programming. 1993, 559– 568
26	P Jančar , J Srba . Undecidability of bisimilarity by Defender’s forcing. Journal of the ACM (JACM), 2008, 55( 1): 5–
27	J Srba. Applications of the existential quantification technique. In: Proceedings of the 4th International Workshop on Verification of Infinite-State Systems (INFINITY02). 2002, 151– 152
28	J Srba . Strong bisimilarity of simple process algebras: Complexity lower bounds. Acta Informatica, 2003, 39( 6−7): 469– 499
29	C Stirling . 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

[1]

Download

[1]	Changbo KE, Fu XIAO, Zhiqiu HUANG, Fangxiong XIAO. A user requirements-oriented privacy policy self-adaption scheme in cloud computing[J]. Front. Comput. Sci., 2023, 17(2): 172203-.
[2]	Xingyue CHEN, Tao SHANG, Feng ZHANG, Jianwei LIU, Zhenyu GUAN. Dynamic data auditing scheme for big data storage[J]. Front. Comput. Sci., 2020, 14(1): 219-229.
[3]	Ying JIANG, Shichao LIU, Thomas EHRHARD. A fully abstract semantics for value-passing CCS for trees[J]. Front. Comput. Sci., 2019, 13(4): 828-849.
[4]	Dan LI,Songtao WANG,Konglin ZHU,Shutao XIA. A survey of network update in SDN[J]. Front. Comput. Sci., 2017, 11(1): 4-12.
[5]	Han XUE,Bing QIN,Ting LIU,Shen LIU. Topic hierarchy construction from heterogeneous evidence[J]. Front. Comput. Sci., 2016, 10(1): 136-146.
[6]	Wanpeng LI, Chunxiang XU, Wenzheng ZHANG, Shixiong ZHU, Xiujie ZHANG. New forward-secure signature schemes with untrusted update[J]. Front Comput Sci, 2013, 7(4): 536-543.
[7]	Quanqing XU , Bin CUI , Yafei DAI , Hengtao SHEN , Zaiben CHEN , Xiaofang ZHOU , . Hybrid information retrieval policies based on cooperative cache in mobile P2P networks[J]. Front. Comput. Sci., 2009, 3(3): 381-395.
[8]	ZHANG Shi, HUANG Linpeng. Research on dynamic update transaction for Java classes[J]. Front. Comput. Sci., 2007, 1(3): 313-321.

Viewed

Full text

Abstract

Cited

Shared

Discussed