×

zbMATH — the first resource for mathematics

The complexity of bisimilarity-checking for one-counter processes. (English) Zbl 1044.68099
Summary: We study the problem of bisimilarity-checking between processes of one-counter automata and finite-state processes. We show that deciding weak bisimilarity between processes of one-counter nets (which are ‘restricted’ one-counter automata where the counter cannot be tested for zero) and finite-state processes is \(\mathbf{DP}\)-hard. In particular, this means that the problem is both \(\mathbf{NP}\) and \(\mathbf{co-NP}\) hard. The same technique is used to demonstrate \(\mathbf{co-NP}\)-hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for a large subclass of instances, giving a kind of characterization of all hard instances as a byproduct. Moreover, we show how to efficiently estimate the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in \(\mathbf P\).
Reviewer: Reviewer (Berlin)

MSC:
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] P.A. Abdulla, K. Čerāns, Simulation is decidable for one-counter nets, in: Proc. CONCUR’98, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1998, pp. 253-268. · Zbl 0940.68055
[2] Abdulla, P.A.; Kindahl, M., Decidability of simulation and bisimulation between lossy channel systems and finite state systems, (), 333-347
[3] Aho, A.V.; Hopcroft, J.E.; Ullman, J.D., The design and analysis of computer algorithms, (1976), Addison-Wesley Reading, MA · Zbl 0207.01701
[4] Bach, E.; Shallit, J., Algorithmic number theory, Vol. 1, efficient algorithms, (1996), The MIT Press Cambridge, MA · Zbl 0873.11070
[5] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Decidability of bisimulation equivalence for processes generating context-free languages, J. assoc. comput. Mach., 40, 653-682, (1993) · Zbl 0801.68102
[6] Baeten, J.C.M.; Weijland, W.P., Process algebra, Cambridge tracts in theoretical computer science, Vol. 18, (1990), Cambridge University Press Cambridge · Zbl 0716.68002
[7] Bouajjani, A.; Esparza, J.; Finkel, A.; Maler, O.; Rossmanith, P.; Willems, B.; Wolper, P., An efficient automata approach to some problems on context-free grammars, Inform. process. lett., 74, 221-227, (2000) · Zbl 1137.68418
[8] Bouajjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automataapplication to model checking, (), 135-150
[9] Burkart, O.; Caucal, D.; Moller, F.; Steffen, B., Verification on infinite structures, (), 545-623 · Zbl 1035.68067
[10] Burkart, O.; Caucal, D.; Steffen, B., An elementary decision procedure for arbitrary context-free processes, (), 423-433 · Zbl 1193.68172
[11] Caucal, D., Graphes canoniques des graphes algébriques, Inform. théor. appl. (RAIRO), 24, 4, 339-352, (1990) · Zbl 0701.68082
[12] Christensen, S.; Hüttel, H.; Stirling, C., Bisimulation equivalence is decidable for all context-free processes, Inform. and comput., 121, 143-148, (1995) · Zbl 0833.68074
[13] Emerson, E.A., Temporal and modal logic, (), 995-1072 · Zbl 0900.03030
[14] Esparza, J.; Hansel, D.; Rossmanith, P.; Schwoon, S., Efficient algorithms for model checking pushdown systems, (), 232-247 · Zbl 0974.68116
[15] Esparza, J.; Knoop, J., An automata-theoretic approach to interprocedural data-flow analysis, (), 14-30
[16] Esparza, J.; Kučera, A.; Schwoon, S., Model-checking LTL with regular valuations for pushdown systems, (), 316-339 · Zbl 1087.68542
[17] Esparza, J.; Rossmanith, P., An automata approach to some problems on context-free grammars, (), 143-152 · Zbl 0895.68085
[18] Groote, J.F., A short proof of the decidability of bisimulation for normed BPA processes, Inform. process. lett., 42, 167-171, (1992) · Zbl 0779.68029
[19] Groote, J.F.; Hüttel, H., Undecidable equivalences for basic process algebra, Inform. and comput., 115, 2, 353-371, (1994) · Zbl 0834.68069
[20] Hirshfeld, Y.; Jerrum, M.; Moller, F., A polynomial algorithm for deciding bisimilarity of normed context-free processes, Theoret. comput. sci., 158, 143-159, (1996) · Zbl 0871.68086
[21] Hopcroft, J.E.; Ullman, J.D., Introduction to automata theory, languages, and computation, (1979), Addison-Wesley Reading, MA · Zbl 0196.01701
[22] Hüttel, H.; Stirling, C., Actions speak louder than wordsproving bisimilarity for context-free processes, J. logic comput., 8, 4, 485-509, (1998) · Zbl 0904.68129
[23] Jančar, P., Decidability of bisimilarity for one-counter processes, Inform. and comput., 158, 1, 1-17, (2000) · Zbl 1046.68621
[24] P. Jančar, A. Kučera, Bisimilarity of processes with finite-state systems, ENTCS, Vol. 9, 1997.
[25] Jančar, P.; Kučera, A.; Mayr, R., Deciding bisimulation-like equivalences with finite-state processes, Theoret. comput. sci., 258, 1-2, 409-433, (2001) · Zbl 0974.68131
[26] Jančar, A. Kučera, P.; Moller, F., Simulation and bisimulation over one-counter processes, (), 334-345 · Zbl 0962.68121
[27] Jančar, P.; Kučera, A.; Moller, F.; Sawa, Z., Equivalence-checking with one-counter automataa generic method for proving lower bounds, (), 172-186 · Zbl 1077.68653
[28] Jančar, P.; Moller, F., Checking regular properties of Petri nets, (), 348-362
[29] Jančar, P.; Moller, F.; Sawa, Z., Simulation problems for one-counter machines, (), 404-413 · Zbl 0963.68094
[30] Kučera, A., On simulation-checking with sequential systems, (), 133-148 · Zbl 0987.68045
[31] Kučera, A.; Mayr, R., On the complexity of semantic equivalences for pushdown automata and BPA, (), 433-445 · Zbl 1014.68103
[32] Kučera, A.; Mayr, R., Simulation preorder over simple process algebras, Inform. and comput., 173, 2, 184-198, (2002) · Zbl 1009.68083
[33] Kučera, A.; Mayr, R., Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time, Theoret. comput. sci., 270, 1-2, 677-700, (2002) · Zbl 0988.68118
[34] R. Mayr, Strict lower bounds for model checking BPA, ENTCS, Vol. 18, 1998.
[35] Mayr, R., On the complexity of bisimulation problems for pushdown automata, (), 474-488 · Zbl 0998.68088
[36] Mayr, R., Process rewrite systems, Inform. and comput., 156, 1, 264-286, (2000) · Zbl 1046.68566
[37] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood, Cliffs, NJ · Zbl 0683.68008
[38] M. Müller-Olm, Derivation of characteristic formulae, ENTCS, Vol. 18, 1998.
[39] Papadimitriou, Ch., Computational complexity, (1994), Addison-Wesley Reading, MA · Zbl 0833.68049
[40] D.M.R. Park, Concurrency and automata on infinite sequences, in: Proc. Fifth GI Conf., Lecture Notes in Computer Science, Vol. 104, Springer, Berlin, 1981, pp. 167-183.
[41] Reisig, W., Petri nets—an introduction, (1985), Springer Berlin · Zbl 0555.68033
[42] G. Sénizergues, Decidability of bisimulation equivalence for equational graphs of finite out-degree, in: Proc. FOCS’98, IEEE, New York, 1998, pp. 120-129.
[43] J. Srba, Strong bisimilarity and regularity of basic process algebra is PSPACE-hard, in: Proc. ICALP 2002, Lecture Notes in Computer Science, Vol. 2380, Springer, Berlin, 2002, pp. 716-727. · Zbl 1057.68071
[44] J. Srba, Undecidability of weak bisimilarity for pushdown processes, in: Proc. CONCUR 2002, Lecture Notes in Computer Science, Vol. 2421, Springer, Berlin, 2002, pp. 579-593. · Zbl 1012.68138
[45] Steffen, B.; Ingólfsdóttir, A., Characteristic formulae for processes with divergence, Inform. and comput., 110, 1, 149-163, (1994) · Zbl 0804.68097
[46] Stirling, C., Decidability of bisimulation equivalence for normed pushdown processes, Theoret. comput. sci., 195, 113-131, (1998) · Zbl 0915.68119
[47] van Glabbeek, R., The linear time—branching time spectrum, (), 3-99 · Zbl 1035.68073
[48] Walukiewicz, I., Model checking CTL properties of pushdown systems, (), 127-138 · Zbl 1044.68111
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.