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

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