Построение приближений бисимуляции в односчетчиковых сетях
Аннотация
Односчетчиковые сети представляют собой конечные автоматы с дополнительным целочисленным неотрицательным счетчиком. Переход управляющего автомата увеличивает или уменьшает значение счетчика, при этом уменьшение возможно только в том случае, когда результат будет неотрицательным; проверка на ноль отсутствует. Односчетчиковые сети эквивалентны по выразительной мощности сетям Петри с не более чем одной неограниченной позицией, а также магазинным автоматам с односимвольным стековым алфавитом.
В работе представлен метод приближения наибольшей бисимуляции в односчетчиковой сети, основанный на использовании однопериодической символьной арифметики и понятия расслоенной бисимуляции.
В работе представлен метод приближения наибольшей бисимуляции в односчетчиковой сети, основанный на использовании однопериодической символьной арифметики и понятия расслоенной бисимуляции.
Об авторе
Владимир Анатольевич Башкин
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
Список литературы
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.
For citation:
Bashkin V.A. Approximating Bisimulation in One-counter Nets. Modeling and Analysis of Information Systems. 2011;18(4):33-44. (In Russ.)
Просмотров: 459
Послать статью по эл. почте 