Abstract
We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between processes of one-counter nets (which are ‘weak’ one-counter automata) and finite-state processes is DP-hard (in particular, it means that the problem is both NP and co-NP hard). The same technique is used to demonstrate 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 most ‘practical’ instances, giving a characterization of all hard instances as a byproduct. Moreover, we show how to efficiently compute a rather tight bound for 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 P.
Supported by the Grant Agency of the Czech Republic, grants No. 201/98/P046 and No. 201/00/0400.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P.A. Abdulla and K. Čerāns. Simulation is decidable for one-counter nets. In Proceedings of CONCUR’98, volume 1466 of LNCS, pages 253–268. Springer, 1998.
E. Bach and J. Shallit. Algorithmic Number Theory. Vol. 1, Efficient Algorithms. The MIT Press, 1996.
S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. Information and Computation, 121:143–148, 1995.
J. Esparza and P. Rossmanith. An automata approach to some problems on context-free grammars. In Foundations of Computer Science, Potential-Theory-Cognition, volume 1337 of LNCS, pages 143–152. Springer, 1997.
J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.
P. Jančar. Bisimulation equivalence is decidable for one-counter processes. In Proceedings of ICALP’97, volume 1256 of LNCS, pages 549–559. Springer, 1997.
P. Jančar, A. Kučera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. In Proceedings of ICALP’98, volume 1443 of LNCS, pages 200–211. Springer, 1998.
P. Jančar, A. Kučera, and F. Moller. Simulation and bisimulation over one-counter processes. In Proceedings of STACS 2000, volume 1770 of LNCS, pages 334–345. Springer, 2000.
P. Jančar, F. Moller, and Z. Sawa. Simulation problems for one-counter machines. In Proceedings of SOFSEM’99, volume 1725 of LNCS, pages 404–413. Springer, 1999.
A. Kučera. Efficient verification algorithms for one-counter processes. Technical report FIMU-RS-2000-03, Faculty of Informatics, Masaryk University, 2000.
A. Kucera and R. Mayr. Weak bisimilarity with infinite-state systems can be decided in polynomial time. In Proceedings of CONCUR’99, volume 1664 of LNCS, pages 368–382. Springer, 1999.
R. Mayr. Private communication. 1999.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
Ch. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
D.M.R. Park. Concurrency and automata on infinite sequences. In Proceedings 5th GI Conference, volume 104 of LNCS, pages 167–183. Springer, 1981.
W. Reisig. Petri Nets—An Introduction. Springer, 1985.
G. Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proceedings of 39th Annual Symposium on Foundations of Computer Science, pages 120–129. IEEE Computer Society Press, 1998.
RJ. van Glabbeek. The linear time—branching time spectrum. In Proceedings of CONCUR’90, volume 458 of LNCS, pages 278–297. Springer, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kučera, A. (2000). Efficient Verification Algorithms for One-Counter Processes. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_28
Download citation
DOI: https://doi.org/10.1007/3-540-45022-X_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67715-4
Online ISBN: 978-3-540-45022-1
eBook Packages: Springer Book Archive