maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-2-139-156mais-212Research ArticleОригинальные статьиArticlesОб эффективном моделировании неограниченного ресурса при помощи односчетчиковых контуровOn the Efficient Representation of an Unbounded Resource with the Aid of One-Counter CircuitsБашкинВладимир АнатольевичBashkinV. A.

канд. физ.-мат. наук, доцент,

150000 Россия, г. Ярославль, ул. Советская, 14

канд. физ.-мат. наук, доцент,

Sovetskaya str., 14, Yaroslavl, 150000, Russia

v_bashkin@mail.ruЯрославский государственный университет им. П. Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation201320042013202139156Copyright © Башкин В.А., 20132013Башкин В.А.Bashkin V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/212

Вводится и исследуется специфический формализм счетчиковых автоматов с одним неограниченным счетчиком без проверки на ноль, обладающий достаточно простым почти периодическим поведением и удобным графическим представлением.

Положительным односчетчиковым контуром называется сильно связная односчетчиковая сеть (недетерминированный конечный автомат с одним счетчиком без проверки на ноль), содержащая по крайней мере один цикл, увеличивающий значение счетчика. Показано, что в положительном контуре бесконечная часть множества достижимости описывается арифметической прогрессией; получены оценки параметров этой прогрессии через структурные свойства диаграммы переходов. Представлен компактный и наглядный способ графического представления контура.

В общем случае односчетчиковые сети обладают такой же выразительной мощностью, как сети Петри с одной неограниченной позицией и магазинные автоматы с односимвольным стековым алфавитом. Показано, что произвольная односчетчиковая сеть может быть представлена в виде конечного дерева односчетчиковых контуров.

Вводится понятие правильно сформированной односчетчиковой сети. Односчетчиковая сеть называется правильно сформированной, если счетчик используется только при порождении бесконечных периодических подмножеств множества достижимых состояний. Показано, что для любой односчетчиковой сети существует эквивалентная (в смысле совпадения множеств достижимости) правильно сформированная сеть, которая может быть эффективно построена из соответствующего дерева контуров.

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.

односчетчиковые сетиVASSсети Петридостижимостьконтурone-counter netsVASSPetri netsreachabilitycircuitРФФИ, Программа "Научные и научно-педагогические кадры инновационной России”ReferencesAbdulla P. A., Čerans K. Simulation is decidable for one-counter nets // CONCUR’98. Lecture Notes in Computer Science. 1998. Vol. 1466. P. 253–268.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.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.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.Башкин В. А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 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]).Башкин В. А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 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]).Башкин В. А. Построение приближений бисимуляции в односчетчиковых сетях // Моделирование и анализ информационных систем. 2011. Т. 18, № 4. С. 34–44 (Bashkin V. A. Approximating Bisimulation in One-counter Nets // MAIS. 2011. Vol. 18, № 4. P. 34–44 [in Russian]).Башкин В. А. Построение приближений бисимуляции в односчетчиковых сетях // Моделирование и анализ информационных систем. 2011. Т. 18, № 4. С. 34–44 (Bashkin V. A. Approximating Bisimulation in One-counter Nets // MAIS. 2011. Vol. 18, № 4. P. 34–44 [in Russian]).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.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.Brauer A. On a Problem of Partitions // American Journal of Mathematics. 1942. 64(1).P. 299–312.Brauer A. On a Problem of Partitions // American Journal of Mathematics. 1942. 64(1).P. 299–312.Erdös P., Graham R. L. On a linear diophantine problem of Frobenius // Acta Arithmetica. 1972. 21. P. 399–408.Erdös P., Graham R. L. On a linear diophantine problem of Frobenius // Acta Arithmetica. 1972. 21. P. 399–408.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.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.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.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.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.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.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.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.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.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.Liubicz U. I. Bounds for the optimal determinization of nondeterministic autonomic automata // Sibirskii Matemat. Journal. 1964. 2. P. 337–355.Liubicz U. I. Bounds for the optimal determinization of nondeterministic autonomic automata // Sibirskii Matemat. Journal. 1964. 2. P. 337–355.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.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.Sylvester J. J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. 41. P. 21.Sylvester J. J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. 41. P. 21.Tarjan R. Depth-First Search and Linear Graph Algorithms // SIAM Journal on Computing. 1972. 1(2). P. 146–160.Tarjan R. Depth-First Search and Linear Graph Algorithms // SIAM Journal on Computing. 1972. 1(2). P. 146–160.

The authors declare that there are no conflicts of interest present.