Об эффективном моделировании неограниченного ресурса при помощи односчетчиковых контуров

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

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

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

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

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.