Об эффективном моделировании неограниченного ресурса при помощи односчетчиковых контуров

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