Geodesic
Approximating bisimulation in one-counter nets
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 33-44.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: one-counter nets, Petri nets, single-periodic base.
Mots-clés : bisimulation 
@article{MAIS_2011_18_4_a3,
     author = {V. A. Bashkin},
     title = {Approximating bisimulation in one-counter nets},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {33--44},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a3/}
}
TY  - JOUR
AU  - V. A. Bashkin
TI  - Approximating bisimulation in one-counter nets
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 33
EP  - 44
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a3/
LA  - ru
ID  - MAIS_2011_18_4_a3
ER  - 
%0 Journal Article
%A V. A. Bashkin
%T Approximating bisimulation in one-counter nets
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 33-44
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a3/
%G ru
%F MAIS_2011_18_4_a3
V. A. Bashkin. Approximating bisimulation in one-counter nets. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 33-44. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a3/

[1] V. A. Bashkin, “Verifikatsiya na osnove modelei s odnim neogranichennym schetchikom”, Informatsionnye sistemy i tekhnologii, 2010, no. 4(60), 5–12

[2] P. A. Abdulla, K. Cerans, “Simulation is decidable for one-counter nets (extended abstract)”, Proc. of CONCUR'98, LNCS, 1466, 1998, 69–153

[3] V. A. Bashkin, “On the single-periodic representation of reachability in one-counter nets”, Proc. of CS'2009, 2009, 60–71

[4] T. Bultan, R. Gerber, W. Pugh, “Symbolic model checking of infinite state systems using Presburger arithmetic”, Proc. of CAV'97, LNCS, 1254, 1997, 400–411

[5] H. Comon, Y. Jurski, “Multiple counters automata, safety analysis and Presburger arithmetic”, Proc. of CAV'98, LNCS, 1427, 1994, 268–279 | MR

[6] S. Ginsburg, E. H. Spanier, “Semigroups, Presburger formulas and languages”, Pacific Journal of Mathematics, 1966, no. 16, 285–296 | MR | Zbl

[7] S. Goller, R. Mayr, A. W. To, “On the Computational Complexity of Verifying One-Counter Processes”, Proc. of LICS'2009, 2009, 235–244

[8] J. E. Hopcroft, J. J. Pansiot, “On the reachability problem for 5-dimensional vector addition systems”, Theor. Comp. Sci., 1979, no. 8(2), 135–159 | DOI | MR | Zbl

[9] P. Jančar, “Decidability questions for bisimilarity of Petri nets and some related problems”, Proc. of STACS'94, LNCS, 775, 1994, 581–592 | MR | Zbl

[10] P. Jančar, F. Moller, “Techniques for decidability and undecidability of bisimilarity”, Proc. of CONCUR'99, LNCS, 1664, 1999, 30–45 | MR | Zbl

[11] P. Jančar, A. Kučera, F. Moller, “Simulation and Bisimulation over One-Counter Processes”, Proc. of STACS'2000, LNCS, 1770, 2000, 334–345 | MR | Zbl

[12] P. Jančar, A. Kučera, F. Moller, Z. Sawa, “DP Lower bounds for equivalence-checking and model-checking of one-counter automata”, Inf. Comput., 2004, no. 188(1), 1–19 | MR

[13] A. Kučera, “Efficient verification algorithms for one-counter processes”, Proc. of ICALP'2000, LNCS 1853, 2000, 317–328 | MR

[14] R. Milner, “A Calculus of Communicating Systems”, Lecture Notes in Computer Science, 92 (1980) | MR | Zbl

[15] D. M. R. Park, Concurrency and automata on infinite sequences, Lecture Notes in Computer Science, 104, 1981 | DOI | Zbl

[16] J. J. Sylvester, “Question 7382”, Mathematical Questions with their Solutions, Educational Times, 41, 1884, 21

[17] L. Valiant, “Deterministic One-Counter Automata”, Journal of Computer and System Sciences, 1975, no. 10, 340–350 | DOI | MR | Zbl