Approximating Bisimulation in One-counter Nets
Abstract
One-counter nets are finite-state machines operating on a variable (counter) which ranges over the natural numbers. Every transition can increase or decrease the value of the counter (the decrease is possible only if the result is non-negative, hence zero-testing is not allowed). The class of one-counter nets is equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet contains one symbol. We present a specific method of approximation of the largest bisimulation of a one-counter net, based on the single-periodic arithmetics and a notion of stratified bisimulation.
About the Author
V. A. Bashkin
Ярославский государственный университет им. П.Г. Демидова
Russian Federation
Russian Federation
References
1. Башкин В.А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 2010. № 4(60). С. 5-12.
2. Abdulla P.A., Cerans K. Simulation is decidable for one-counter nets (extended abstract)// Proc. of CONCUR'98. 1998. LNCS 1466. P. 69-153.
3. Bashkin V.A. On the single-periodic representation of reachability in one-counter nets // Proc. of CS&P'2009 (Warsaw). 2009. P. 60-71.
4. Bultan T., Gerber R., Pugh W. Symbolic model checking of infinite state systems using Presburger arithmetic // Proc. of CAV'97. 1997. LNCS 1254. P. 400-411.
5. Comon H., Jurski Y. Multiple counters automata, safety analysis and Presburger arithmetic // Proc. of CAV'98. 1994. LNCS 1427. P. 268-279.
6. Ginsburg S., Spanier E.H. Semigroups, Presburger formulas and languages // Pacific Journal of Mathematics. 1966. № 16. P. 285-296.
7. Goller S., Mayr R., To A.W. On the Computational Complexity of Verifying One- Counter Processes // Proc. of LICS'2009. 2009. P. 235-244.
8. Hopcroft J.E., Pansiot J.-J. On the reachability problem for 5-dimensional vector addition systems // Theor. Comp. Sci. 1979. № 8(2). P. 135-159.
9. Jancar P. Decidability questions for bisimilarity of Petri nets and some related problems // Proc. of STACS'94. 1994. LNCS 775. P. 581-592.
10. Jancar P., Moller F. Techniques for decidability and undecidability of bisimilarity // Proc. of CONCUR'99. 1999. LNCS 1664. P. 30-45.
11. Jancar P., Kucera A., Moller F. Simulation and Bisimulation over One-Counter Processes // Proc. of STACS'2000. 2000. LNCS 1770. P. 334-345.
12. Jancar P., Kucera A., Moller F., Sawa Z. DP Lower bounds for equivalence-checking and model-checking of one-counter automata // Inf. Comput. 2004. № 188(1). P. 1-19.
13. Kucera A. Efficient verification algorithms for one-counter processes // Proc. of ICALP'2000. 2000. LNCS 1853. P. 317-328.
14. Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. 1980. V. 92.
15. Park D.M.R. Concurrency and automata on infinite sequences // Lecture Notes in Computer Science. 1981. V. 104.
16. Sylvester J.J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. Vol. 41. P. 21.
17. Valiant L. Deterministic One-Counter Automata // Journal of Computer and System Sciences. 1975. № 10. P. 340-350.
Review
For citations:
Bashkin V.A. Approximating Bisimulation in One-counter Nets. Modeling and Analysis of Information Systems. 2011;18(4):33-44. (In Russ.)
Views:
488
Email this article 