maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1096Research ArticleОригинальные статьиArticlesПостроение приближений бисимуляции в односчетчиковых сетяхApproximating Bisimulation in One-counter NetsБашкинВладимир АнатольевичBashkinV. A.bas@uniyar.ac.ruЯрославский государственный университет им. П.Г. ДемидоваRussian Federation2011201220111843344Copyright © Башкин В.А., 20112011Башкин В.А.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/1096

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

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.

односчетчиковые сетисети Петрибисимуляцияоднопериодический базисone-counter netsPetri netsbisimulationsingle-periodic baseReferencesБашкин В.А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 2010. № 4(60). С. 5-12.Башкин В.А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 2010. № 4(60). С. 5-12.Abdulla P.A., Cerans K. Simulation is decidable for one-counter nets (extended abstract)// Proc. of CONCUR'98. 1998. LNCS 1466. P. 69-153.Abdulla P.A., Cerans K. Simulation is decidable for one-counter nets (extended abstract)// Proc. of CONCUR'98. 1998. LNCS 1466. P. 69-153.Bashkin V.A. On the single-periodic representation of reachability in one-counter nets // Proc. of CS&P'2009 (Warsaw). 2009. P. 60-71.Bashkin V.A. On the single-periodic representation of reachability in one-counter nets // Proc. of CS&P'2009 (Warsaw). 2009. P. 60-71.Bultan T., Gerber R., Pugh W. Symbolic model checking of infinite state systems using Presburger arithmetic // Proc. of CAV'97. 1997. LNCS 1254. P. 400-411.Bultan T., Gerber R., Pugh W. Symbolic model checking of infinite state systems using Presburger arithmetic // Proc. of CAV'97. 1997. LNCS 1254. P. 400-411.Comon H., Jurski Y. Multiple counters automata, safety analysis and Presburger arithmetic // Proc. of CAV'98. 1994. LNCS 1427. P. 268-279.Comon H., Jurski Y. Multiple counters automata, safety analysis and Presburger arithmetic // Proc. of CAV'98. 1994. LNCS 1427. P. 268-279.Ginsburg S., Spanier E.H. Semigroups, Presburger formulas and languages // Pacific Journal of Mathematics. 1966. № 16. P. 285-296.Ginsburg S., Spanier E.H. Semigroups, Presburger formulas and languages // Pacific Journal of Mathematics. 1966. № 16. P. 285-296.Goller S., Mayr R., To A.W. On the Computational Complexity of Verifying One- Counter Processes // Proc. of LICS'2009. 2009. P. 235-244.Goller S., Mayr R., To A.W. On the Computational Complexity of Verifying One- Counter Processes // Proc. of LICS'2009. 2009. P. 235-244.Hopcroft J.E., Pansiot J.-J. On the reachability problem for 5-dimensional vector addition systems // Theor. Comp. Sci. 1979. № 8(2). P. 135-159.Hopcroft J.E., Pansiot J.-J. On the reachability problem for 5-dimensional vector addition systems // Theor. Comp. Sci. 1979. № 8(2). P. 135-159.Jancar P. Decidability questions for bisimilarity of Petri nets and some related problems // Proc. of STACS'94. 1994. LNCS 775. P. 581-592.Jancar P. Decidability questions for bisimilarity of Petri nets and some related problems // Proc. of STACS'94. 1994. LNCS 775. P. 581-592.Jancar P., Moller F. Techniques for decidability and undecidability of bisimilarity // Proc. of CONCUR'99. 1999. LNCS 1664. P. 30-45.Jancar P., Moller F. Techniques for decidability and undecidability of bisimilarity // Proc. of CONCUR'99. 1999. LNCS 1664. P. 30-45.Jancar P., Kucera A., Moller F. Simulation and Bisimulation over One-Counter Processes // Proc. of STACS'2000. 2000. LNCS 1770. P. 334-345.Jancar P., Kucera A., Moller F. Simulation and Bisimulation over One-Counter Processes // Proc. of STACS'2000. 2000. LNCS 1770. P. 334-345.Jancar P., Kucera A., Moller F., Sawa Z. DP Lower bounds for equivalence-checking and model-checking of one-counter automata // Inf. Comput. 2004. № 188(1). P. 1-19.Jancar P., Kucera A., Moller F., Sawa Z. DP Lower bounds for equivalence-checking and model-checking of one-counter automata // Inf. Comput. 2004. № 188(1). P. 1-19.Kucera A. Efficient verification algorithms for one-counter processes // Proc. of ICALP'2000. 2000. LNCS 1853. P. 317-328.Kucera A. Efficient verification algorithms for one-counter processes // Proc. of ICALP'2000. 2000. LNCS 1853. P. 317-328.Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. 1980. V. 92.Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. 1980. V. 92.Park D.M.R. Concurrency and automata on infinite sequences // Lecture Notes in Computer Science. 1981. V. 104.Park D.M.R. Concurrency and automata on infinite sequences // Lecture Notes in Computer Science. 1981. V. 104.Sylvester J.J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. Vol. 41. P. 21.Sylvester J.J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. Vol. 41. P. 21.Valiant L. Deterministic One-Counter Automata // Journal of Computer and System Sciences. 1975. № 10. P. 340-350.Valiant L. Deterministic One-Counter Automata // Journal of Computer and System Sciences. 1975. № 10. P. 340-350.

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