On the Efficient Representation of an Unbounded Resource with the Aid of One-Counter Circuits
https://doi.org/10.18255/1818-1015-2013-2-139-156
Abstract
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.
About the Author
V. A. Bashkin
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
канд. физ.-мат. наук, доцент,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
References
1. Abdulla P. A., Čerans K. Simulation is decidable for one-counter nets // CONCUR’98. Lecture Notes in Computer Science. 1998. Vol. 1466. P. 253–268.
2. Bashkin V. A., Lomazova I. A. Resource similarities in Petri net models of distributed systems // PaCT’2003. Lecture Notes in Computer Science. 2003. Vol. 2763. P. 35–48.
3. Башкин В. А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 2010. № 4(60). С. 5–12 (Bashkin V. A. Verification based on the models with a single unbounded counter // Information Systems and Technologies. 2010. № 4(60). P. 5–12 [in Russian]).
4. Башкин В. А. Построение приближений бисимуляции в односчетчиковых сетях // Моделирование и анализ информационных систем. 2011. Т. 18, № 4. С. 34–44 (Bashkin V. A. Approximating Bisimulation in One-counter Nets // MAIS. 2011. Vol. 18, № 4. P. 34–44 [in Russian]).
5. Bashkin V. A. One-counter Circuits // Concurrency, Specification and Programming. CSP 2012 Workshop Proceedings. Vol. 1. Berlin, Germany: Humboldt-Universitat zu Berlin, 2012. P. 25–36.
6. Brauer A. On a Problem of Partitions // American Journal of Mathematics. 1942. 64(1).P. 299–312.
7. Erdös P., Graham R. L. On a linear diophantine problem of Frobenius // Acta Arithmetica. 1972. 21. P. 399–408.
8. Göller S., Haase C., Ouaknine J., Worrell J. Model checking succinct and parametric onecounter automata // Automata, Languages and Programming. Lecture Notes in Computer Science. 2010. Vol. 6199. P. 575–586.
9. Göller S., R. Mayr, To A.W. On the computational complexity of verifying one-counter processes // Proc. of LICS ’09, IEEE Computer Society, Washington, DC, USA, 2009.
10. Jančar P., Kučera A., Moller F., Sawa Z. DP lower bounds for equivalence-checking and model-checking of one-counter automata // Information and Computation. 2004. 188(1). P. 1–19.
11. Kučera A. Efficient verification algorithms for one-counter processes // Automata, Languages and Programming. Lecture Notes in Computer Science. 2000. Vol. 1853. P. 317–328.
12. Kuzmin E. V., Chalyy D.Ju. On the Reachability Set of Automaton Counter Machines // Automatic Control and Computer Sciences. 2011. Vol. 45, No. 7. P. 444–451.
13. Liubicz U. I. Bounds for the optimal determinization of nondeterministic autonomic automata // Sibirskii Matemat. Journal. 1964. 2. P. 337–355.
14. Serre O. Parity games played on transition graphs of one-counter processes // Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science. 2006. Vol. 3921. P. 337–351.
15. Sylvester J. J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. 41. P. 21.
16. Tarjan R. Depth-First Search and Linear Graph Algorithms // SIAM Journal on Computing. 1972. 1(2). P. 146–160.
Review
For citations:
Bashkin V.A. On the Efficient Representation of an Unbounded Resource with the Aid of One-Counter Circuits. Modeling and Analysis of Information Systems. 2013;20(2):139-156. (In Russ.) https://doi.org/10.18255/1818-1015-2013-2-139-156
Views:
904
Email this article 