On a reachability set of automaton counter machines
Abstract
Properties of automaton counter machines are investigated. We prove that reachability sets of automaton one-counter machines are semilinear. An algorithm of construction of these semilinear reachability sets is resultexl. Besides, it is shown that reachability sets of reversal-boundexl automaton counter machines and reachability sets of hat automaton counter machines are also semilinear.
About the Authors
E. V. Kuzmin
Ярославский государственный университет им. П.Г. Демидова
Russian Federation
Russian Federation
D. J. Chalyy
Ярославский государственный университет им. П.Г. Демидова
Russian Federation
Russian Federation
References
1. Annichini A., Bouajjani A., Sighireanu M. TReX: A tool for reachability analysis of complex systems // LNCS 2102, Springer, 2001. P. 368-372.
2. Araki T., Kasami T. Decidable problems on the strong connectivity of Petri net reachability sets // Theoretical Computer Science, 4(1), 1977. P. 99-119.
3. Bardin S., Leroux J., Point G. FAST extended release // LNCS 4144, Springer, 2006. P. 63-66.
4. Esparza J. Petri nets, commutative context-free grammars, and basic parallel processes // Fundamenta Informatica, 31(1), 1997. P. 13-25.
5. Finkel A., Leroux J. How to compose Presburger-accelerations: Applications to broadcast protocols // LNCS 2556, Springer, 2002. P. 145-156.
6. Finkel A., Sangnier A. Reversal-bounded Counter Machines Revisited // LNCS 5162, Springer, 2008. P. 323-334.
7. Hopcroft J. E., Pansiot J. On the Reachability Problem for 5-Dimensional Vector Addition Systems. Computer science technical report. Cornell University, 1976. - http://hdl.handle.net/1813/6102
8. Ibarra O. H. Reversal-bounded multicounter machines and their decision problems // J. ACM, 25(1), 1978. P. 116-133.
9. Konig D. Theorie der Endlichen und Unendlichen Graphen // Akademische Verlagsgesellschaft, Leipzig, 1936.
10. Kouzmin E. V., Sokolov V.A. Communicating Colouring Automata // Proc. Int. Workshop on Program Understanding (sat. of PSI'03), 2003. P. 40-46.
11. Kuzmin E. V., Sokolov V. A., Chaly D. Ju. Automaton Counter Machines // Proc. of Int. Workshop on Program Understanding (sat. of PSI'09), 2009. P. 1-4.
12. LASH. http://www.montefiore.ulg.ac.be/~boigelot/research/lash
13. Leroux J., Sutre G. Flat counter almost everywhere! // LNCS 3707, Springer, 2005. P. 474-488.
14. Mayr E. W. Persistence of vector replacement systems is decidable // Acta Informatica, 15, 1981. P. 309-318.
15. Mayr E. W. An algorithm for the general Petri net reachability problem // SIAM J. Comput., 13(3), 1984. P. 441-460.
16. Presburger M. Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt / M. Presburger // Sprawozdanie z I Kongresu matematykow krajow slowianskich, Warszawa 1929, Warsaw, 1930. P. 92-101, 395.
17. Valk R., Vidal-Naquet G. Petri nets and regular languages // J. Comput. Syst. Sci., 23(3), 1981. P. 299-325.
18. Гинзбург С. Математическая теория контекстно-свободных языков. М.:Мир, 1970. 328 с.
19. Кузьмин Е. В., Соколов В. А. Взаимодействующие раскрашивающие процессы // Моделирование и анализ информационных систем. 2004. Т. 11, №2. С. 8-17.
20. Кузьмин Е. В., Чалый Д. Ю. Об одном классе счетчиковых машин // Модели¬рование и анализ информационных систем. 2009. Т. 16, №2. С. 75-82.
21. Кузьмин Е. В. , Чалый Д. Ю. О множестве достижимости автоматных трех-счетчиковых машин // Моделирование и анализ информационных систем. 2009. Т. 16, №3. С. 77-84.
22. Минский М. Вычисления и автоматы. М.: Мир, 1971. 268 c.
Review
For citations:
Kuzmin E.V., Chalyy D.J. On a reachability set of automaton counter machines. Modeling and Analysis of Information Systems. 2010;17(1):52-64. (In Russ.)
Views:
513
Email this article 