Geodesic
On the Efficient Representation of an Unbounded Resource with the Aid of~One-Counter Circuits
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 2, pp. 139-156.

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

A class of infinite-state automata with a simple periodic behaviour and a convenient graphical representation is studied. A positive one-counter circuit is defined as a strongly connected one-counter net (one-counter nondeterministic finite automata without zero-testing) with at least one positive cycle. It is shown that in a positive circuit an infinite part of a reachability set is an arithmetic progression; numerical properties of this progression are estimated. A specific graphical representation of circuits is presented. General one-counter nets are equivalent to Petri Nets with at most one unbounded place and to pushdown automata with a single-symbol stack alphabet. It is shown that an arbitrary one-counter net can be represented by a finite tree of circuits. A one-counter net is called sound, if a counter is used only for “infinite-state” (periodic) behaviour. It is shown that for an arbitrary one-counter net an equivalent sound net can be effectively constructed from the corresponding tree of circuits.
Keywords: one-counter nets, Petri nets, reachability
Mots-clés : VASS, circuit. 
@article{MAIS_2013_20_2_a10,
     author = {V. A. Bashkin},
     title = {On the {Efficient} {Representation} of an {Unbounded} {Resource} with the {Aid} {of~One-Counter} {Circuits}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {139--156},
     publisher = {mathdoc},
     volume = {20},
     number = {2},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a10/}
}
TY  - JOUR
AU  - V. A. Bashkin
TI  - On the Efficient Representation of an Unbounded Resource with the Aid of~One-Counter Circuits
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 139
EP  - 156
VL  - 20
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a10/
LA  - ru
ID  - MAIS_2013_20_2_a10
ER  - 
%0 Journal Article
%A V. A. Bashkin
%T On the Efficient Representation of an Unbounded Resource with the Aid of~One-Counter Circuits
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 139-156
%V 20
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a10/
%G ru
%F MAIS_2013_20_2_a10
V. A. Bashkin. On the Efficient Representation of an Unbounded Resource with the Aid of~One-Counter Circuits. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 2, pp. 139-156. http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a10/

[1] P. A. Abdulla, K. Čerans, “Simulation is decidable for one-counter nets”, CONCUR'98, Lecture Notes in Computer Science, 1466, 1998, 253–268 | DOI | Zbl

[2] V. A. Bashkin, I. A. Lomazova, “Resource similarities in Petri net models of distributed systems”, PaCT'2003, Lecture Notes in Computer Science, 2763, 2003, 35–48 | DOI

[3] V. A. Bashkin, “Verification based on the models with a single unbounded counter”, Information Systems and Technologies, 2010, no. 4(60), 5–12 (in Russian)

[4] V. A. Bashkin, “Approximating Bisimulation in One-counter Nets”, MAIS, 18:4 (2011), 34–44 (in Russian) | MR

[5] V. A. Bashkin, “One-counter Circuits”, Concurrency, Specification and Programming, CSP 2012 Workshop Proceedings, v. 1, Humboldt-Universitat zu Berlin, Berlin, Germany, 2012, 25–36

[6] A. Brauer, “On a {P}roblem of {P}artitions”, American Journal of Mathematics, 64:1 (1942), 299–312 | DOI | MR | Zbl

[7] P. Erdös, R. L. Graham, “On a linear diophantine problem of {F}robenius”, Acta Arithmetica, 21 (1972), 399–408 | MR | Zbl

[8] S. Göller, C. Haase, J. Ouaknine, J. Worrell, “Model checking succinct and parametric one-counter automata”, Automata, Languages and Programming, Lecture Notes in Computer Science, 6199, 2010, 575–586 | DOI | MR

[9] S. Göller, R. Mayr, A. W. To, “On the computational complexity of verifying one-counter processes”, Proc. of LICS '09, IEEE Computer Society, Washington, DC, USA, 2009 | MR

[10] P. Jančar, A. Kučera, F. Moller, Z. Sawa, “DP lower bound for equivalence-checking and model-checking of one-counter automata”, Information and Computation, 188:1 (2004), 1–19 | DOI | MR | Zbl

[11] A. Kučera, “Efficient verification algorithms for one-counter processes”, Automata, Languages and Programming, Lecture Notes in Computer Science, 1853, 2000, 317–328 | DOI | MR

[12] E. V. Kuzmin, D. Ju. Chalyy, “On the Reachability Set of Automaton Counter Machines”, Automatic Control and Computer Sciences, 45:7 (2011), 444–451 | DOI

[13] U. I. Liubicz, “Bounds for the optimal determinization of nondeterministic autonomic automata”, Sibirskii Matemat. Journal, 2 (1964), 337–355

[14] O. Serre, “Parity games played on transition graphs of one-counter processes”, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, 3921, 2006, 337–351 | DOI | MR | Zbl

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

[16] R. Tarjan, “Depth-First Search and Linear Graph Algorithms”, SIAM Journal on Computing, 1:2 (1972), 146–160 | DOI | MR | Zbl