maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-970Research ArticleОригинальные статьиArticlesО разрешимости проблем ограниченности для счетчиковых машин МинскогоOn the decidability of boundedness problems for counter Minsky machinesКузьминЕ. В.KuzminE. V.noemail@neicon.ruЧалыйД. Ю.ChalyyD. Ju.noemail@neicon.ruЯрославский государственный университетRussian Federation2008200320081511626Copyright © Кузьмин Е.В., Чалый Д.Ю., 20082008Кузьмин Е.В., Чалый Д.Ю.Kuzmin E.V., Chalyy D.J.Данная работа распространяется под лицензией 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/970

Исследуется разрешимость проблем ограниченности для счетчиковых машин Минского. Доказывается, что для машин Минского с двумя счетчиками проблема ограниченности лишь частично разрешима, а проблема тотальной ограниченности не является даже частично разрешимой. Для односчет-чиковых машин Минского указанные проблемы разрешимы за время, полиномиально зависящее от общего количества локальных состояний счетчиковой машины.

In the paper the decidability of boundedness problems for counter Minsky machines is investigated. It is proved, that for Minsky machines with two counters the boundedness is partial decidable, but for the total boundedness problem does not even exist a semidecision algorithm. On the other hand, for one-counter Minsky machines all these problems are polinomial (quantitatively of local machine states) decidable.

ReferencesКларк, Э.М. Верификация моделей программ: Model Checking / Э.М. Кларк, О. Грамберг, Д. Пелед. - МЦНМО, 2002. - 416 с.Кларк, Э.М. Верификация моделей программ: Model Checking / Э.М. Кларк, О. Грамберг, Д. Пелед. - МЦНМО, 2002. - 416 с.Котов, В.Е. Сети Петри / В.Е. Котов - М.: Наука, 1984. - 160 с.Котов, В.Е. Сети Петри / В.Е. Котов - М.: Наука, 1984. - 160 с.Котов, В.Е. Теория схем программ /В.Е. Котов, В. К. Сабельфельд. - М.: Наука, 1991. - 248 с.Котов, В.Е. Теория схем программ /В.Е. Котов, В. К. Сабельфельд. - М.: Наука, 1991. - 248 с.Кузьмин, Е. В. Структурированные системы переходов / Е. В. Кузьмин, В. А. Соколов. - М.: ФИЗ-МАТЛИТ, 2006. - 178 с.Кузьмин, Е. В. Структурированные системы переходов / Е. В. Кузьмин, В. А. Соколов. - М.: ФИЗ-МАТЛИТ, 2006. - 178 с.Минский, М. Вычисления и автоматы / М. Минский - М.: Мир, 1971. - 268 с.Минский, М. Вычисления и автоматы / М. Минский - М.: Мир, 1971. - 268 с.Хопкрофт, Д. Введение в теорию автоматов, языков и вычислений / Д. Хопкрофт, Р. Мотвани, Д. Уль¬ман. - 2-е изд.: Пер. с англ. - М.: Вильямс, 2002. - 528 с.Хопкрофт, Д. Введение в теорию автоматов, языков и вычислений / Д. Хопкрофт, Р. Мотвани, Д. Уль¬ман. - 2-е изд.: Пер. с англ. - М.: Вильямс, 2002. - 528 с.Chitic, C. On validation of XML streams using finite state machines / C. Chitic, D. Rosu. - WebDB, Paris, 2004. - P. 85-90.Chitic, C. On validation of XML streams using finite state machines / C. Chitic, D. Rosu. - WebDB, Paris, 2004. - P. 85-90.Demri, S. Model checking freeze LTL over one-counter automata / S. Demri, R. Lazic, A. Sangnier // Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), LNCS. - 2008. To appear. (http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf).Demri, S. Model checking freeze LTL over one-counter automata / S. Demri, R. Lazic, A. Sangnier // Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), LNCS. - 2008. To appear. (http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf).Dufourd, C. Boundedness of Reset P/T nets / C. Dufourd, P. Jancar, Ph. Schnoebelen // Proc. ICALP'99, LNCS 1644. - 1999. - P. 301-310.Dufourd, C. Boundedness of Reset P/T nets / C. Dufourd, P. Jancar, Ph. Schnoebelen // Proc. ICALP'99, LNCS 1644. - 1999. - P. 301-310.Lafourcade, P. Intruder deduction for AC-like equational theories with homomorphisms / P. Lafourcade, D. Lugiez, R. Treinen. - RTA'05, LNCS 3467, Springer, 2005. - P. 308-322.Lafourcade, P. Intruder deduction for AC-like equational theories with homomorphisms / P. Lafourcade, D. Lugiez, R. Treinen. - RTA'05, LNCS 3467, Springer, 2005. - P. 308-322.Mayr R. Lossy counter machines / R. Mayr // Tech. Report TUM-I9827, Institut fur Informatik, TUM, Germany, October 1998.Mayr R. Lossy counter machines / R. Mayr // Tech. Report TUM-I9827, Institut fur Informatik, TUM, Germany, October 1998.Wakatsuki, M. Polynomial time identification of strict deterministic restricted one-counter automata in some class from positive data / M. Wakatsuki, K. Teraguchi, E. Tomita. - ICGI 2004, Athens, LNAI 3264, Springer, 2004. - P. 260-272.Wakatsuki, M. Polynomial time identification of strict deterministic restricted one-counter automata in some class from positive data / M. Wakatsuki, K. Teraguchi, E. Tomita. - ICGI 2004, Athens, LNAI 3264, Springer, 2004. - P. 260-272.

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