Построение приближений бисимуляции в односчетчиковых сетях


https://doi.org/10.18255/1818-1015-2011-4-33-44

Полный текст:


Аннотация

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

Об авторе

Владимир Анатольевич Башкин
Ярославский государственный университет им. П.Г. Демидова
Россия


Список литературы

1. Башкин В.А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии. 2010. № 4(60). С. 5-12.

2. Abdulla P.A., Cerans K. Simulation is decidable for one-counter nets (extended abstract)// Proc. of CONCUR'98. 1998. LNCS 1466. P. 69-153.

3. Bashkin V.A. On the single-periodic representation of reachability in one-counter nets // Proc. of CS&P'2009 (Warsaw). 2009. P. 60-71.

4. 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.

5. Comon H., Jurski Y. Multiple counters automata, safety analysis and Presburger arithmetic // Proc. of CAV'98. 1994. LNCS 1427. P. 268-279.

6. Ginsburg S., Spanier E.H. Semigroups, Presburger formulas and languages // Pacific Journal of Mathematics. 1966. № 16. P. 285-296.

7. Goller S., Mayr R., To A.W. On the Computational Complexity of Verifying One- Counter Processes // Proc. of LICS'2009. 2009. P. 235-244.

8. 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.

9. Jancar P. Decidability questions for bisimilarity of Petri nets and some related problems // Proc. of STACS'94. 1994. LNCS 775. P. 581-592.

10. Jancar P., Moller F. Techniques for decidability and undecidability of bisimilarity // Proc. of CONCUR'99. 1999. LNCS 1664. P. 30-45.

11. Jancar P., Kucera A., Moller F. Simulation and Bisimulation over One-Counter Processes // Proc. of STACS'2000. 2000. LNCS 1770. P. 334-345.

12. 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.

13. Kucera A. Efficient verification algorithms for one-counter processes // Proc. of ICALP'2000. 2000. LNCS 1853. P. 317-328.

14. Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. 1980. V. 92.

15. Park D.M.R. Concurrency and automata on infinite sequences // Lecture Notes in Computer Science. 1981. V. 104.

16. Sylvester J.J. Question 7382 // Mathematical Questions with their Solutions, Educational Times. 1884. Vol. 41. P. 21.

17. Valiant L. Deterministic One-Counter Automata // Journal of Computer and System Sciences. 1975. № 10. P. 340-350.


Дополнительные файлы

Для цитирования: Башкин В.А. Построение приближений бисимуляции в односчетчиковых сетях. Моделирование и анализ информационных систем. 2011;18(4):33-44. https://doi.org/10.18255/1818-1015-2011-4-33-44

For citation: Bashkin V.A. Approximating Bisimulation in One-counter Nets. Modeling and Analysis of Information Systems. 2011;18(4):33-44. (In Russ.) https://doi.org/10.18255/1818-1015-2011-4-33-44

Просмотров: 3

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)