zbMATH — the first resource for mathematics

Decidability of bisimilarity for one-counter processes. (English) Zbl 1046.68621
Summary: It is shown that bisimulation equivalence is decidable for the processes generated by (nondeterministic) pushdown automata, where the pushdown behaves like a counter. Also finiteness up to bisimilarity is shown to be decidable for the mentioned processes.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI
[1] Abdulla, P.; Čerāns, K., Simulation is decidable for one-counter nets, Proceedings, CONCUR’98, Lecture notes in computer science, 1466, (1998), Springer-Verlag New York/Berlin, p. 253-268 · Zbl 0940.68055
[2] Burkart, O.; Caucal, D.; Steffen, B., Bisimulation collapse and the process taxonomy, Proceedings, CONCUR’96, Lecture notes in computer science, 1119, (1996), Springer-Verlag New York/Berlin, p. 247-262
[3] Christensen, S.; Hirshfeld, Y.; Moller, F., Bisimulation equivalence is decidable for all basic parallel processes, Proceedings, CONCUR’93, Lecture notes in computer science, 715, (1993), Springer-Verlag New York/Berlin, p. 143-157
[4] 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
[5] Esparza, J., Petri nets, commutative context-free grammars, and basic parallel processes, Proceedings. fundamentals of computation theory (FCT) 1995, Lecture notes in computer science, 965, (1995), Springer-Verlag New York/Berlin, p. 221-232
[6] Ginsburg, S.; Spanier, E., Semigroups, Presburger formulas, and languages, Pacific J. math., 16, 285-296, (1966) · Zbl 0143.01602
[7] Hirshfeld, Y., Petri nets and the equivalence problem, Proceedings, computer science logic (CSL)’93, Lecture notes in computer science, 832, (1994), Springer-Verlag New York/Berlin, p. 165-174 · Zbl 0953.68571
[8] Jančar, P., Decidability questions for bisimilarity of Petri nets and some related problems, Tech. rep., (1993)
[9] Jančar, P., Undecidability of bisimilarity for Petri nets and related problems, Theoret. comput. sci., 148, 281-301, (1995) · Zbl 0873.68147
[10] Jančar, P.; Esparza, J., Deciding finiteness of Petri nets up to bisimulation, Proceedings, ICALP’96, Lecture notes in computer science, 1099, (1996), Springer-Verlag New York/Berlin, p. 478-489 · Zbl 1046.68622
[11] Jančar, P.; Moller, F., Checking regular properties of Petri nets, Proceedings, CONCUR’95, Lecture notes in computer science, 962, (1995), Springer-Verlag New York/Berlin, p. 348-362
[12] Jančar, P.; Moller, F., Simulation of one-counter nets via colouring, Proceedings, journées systèmes infinis, LSV ENS, cachan, France, (1998), p. 1-6
[13] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs · Zbl 0683.68008
[14] Oppen, D.C., A 2^2^2^pn upper bound on the complexity of Presburger arithmetic, J. comput. system sci., 16, 323-332, (1978) · Zbl 0381.03021
[15] Sénizergues, G., The equivalence problem for deterministic pushdown automata is decidable, Proceedings, ICALP’97, Lecture notes in computer science, 1256, (1997), Springer-Verlag New York/Berlin, p. 671-681 · Zbl 1401.68168
[16] Stirling, C., Decidability of bisimulation equivalence for normed pushdown processes, Proceedings, CONCUR’96, Lecture notes in computer science, 1119, (1996), Springer-Verlag New York/Berlin, p. 217-232
[17] Valiant, L.G.; Paterson, M.S., Deterministic one-counter automata, J. comput. system sci., 10, 340-350, (1975) · Zbl 0307.68038
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.