ДОКЛАДЫ АКАДЕМИИ НАУК, 2008, том 421, № 6, с. 741-743
= МАТЕМАТИКА
УДК 519.7
ПРОБЛЕМЫ ОГРАНИЧЕННОСТИ СЧЕТЧИКОВЫХ МАШИН МИНСКОГО
© 2008 г. Е. В. Кузьмин, В. А. Соколов, Д. Ю. Чалый
Представлено академиком Ю.И. Журавлевым 28.03.2008 г. Поступило 28.04.2008 г.
В статье исследуется разрешимость проблем ограниченности и тотальной ограниченности для счетчиковых машин Минского [5]. Рассмотрение счетчиковых машин здесь проводится с точки зрения моделирования и анализа программных систем. Давно уже стал стандартным прием использования абстрактных счетчиковых машин в качестве общего средства для демонстрации алгоритмической неразрешимости ряда проблем для формальных моделей программных и аппаратных систем, способных моделировать поведение этих машин. В частности, все неразрешимые проблемы для машин Минского автоматически переходят и на сети Петри с ингибиторными дугами и сети Петри с приоритетами [2], неразрешимость проблем счетчиковых машин с потерями [11] ведет к неразрешимости тех же проблем для сетей Петри с обнуляющими дугами, FIFO-канальных систем с потерями и т.д.
Исследуемая в сообщении проблема ограниченности является одной из самых важных для теории формальных моделей, поскольку в случае разрешимости позволяет определять, является ли множество состояний модели программной системы конечным, что критично, например, для автоматического метода верификации model checking [1]. К сожалению, как будет показано далее, для двухсчетчиковых машин Минского проблема ограниченности лишь частично разрешима, а проблема тотальной ограниченности не является даже частично разрешимой. Интересно, что в литературе проблеме ограниченности для каждого отдельного формализма уделяется довольно много внимания. Однако ограниченность непосредственно для счетчиковых машин Минского практически не исследовалась. Отметим лишь, что в работе [9] факт ограниченности двухсчетчиковых машин как очевидное следствие того, что машина Минского с двумя счетчиками может моделировать машину Тьюринга [5], был бездоказа-
тельно использован для анализа сетей Петри с обнуляющими дугами.
Особого внимания заслуживают односчетчи-ковые машины Минского. Несмотря на наличие всего лишь одного счетчика, абстрактные машины этого класса имеют широкий спектр применения, например, для верификации криптографических протоколов [10], валидации XML потоков [7] и решения задачи идентификации [12]. Кроме того, односчетчиковые машины могут быть промоделированы специальным подклассом магазинных автоматов, алфавит которых состоит только из одного символа [6]. В данном сообщении показывается разрешимость за полиномиальное время проблем ограниченности и тотальной ограниченности. Более того, из леммы о конечном пути, задающем полное исполнение (возможно, бесконечное) односчетчиковой машины, из [8], можно также говорить и о полиномиальной разрешимости задач достижимости, останова, тотальности, пустоты и т.п.
СЧЕТЧИКОВЫЕ МАШИНЫ МИНСКОГО
Счетчиковая машина Минского M - это набор (1?0, ?1, •••, ?«}, 1*1, *2, •••, Xm}, (So, Si, ..., 5И- i}), где Xj - счетчик, qi - состояние, q0 - начальное состояние, qn - финальное (заключительное) состояние, Si - правило перехода для qj, 0 < i < n - 1.
Состояния qi, 0 < i < n - 1, подразделяются на два типа. Состояния первого типа имеют правила переходов вида
Sj: Xj := Xj +1; goto qk,
где 1 < j < m, 0 < k, l < n. Для состояний второго типа имеем
Si: if Xj > 0 then (Xj := Xj - 1; goto qk) else goto .
Конфигурация машины Минского представляет собой набор (qi, с1, с2, ..., cm), где qi - состояние машины, c1, c2, ..., cm - натуральные числа (включая ноль), являющиеся значениями соответствующих счетчиков.
Ярославский государственный университет им. П.Г. Демидова
742
КУЗЬМИН и др.
Исполнение счетчнковой машины - это последовательность конфигураций ^ ^ ^ S2 ^ ... с начальной конфигурацией % индуктивно определяемая в соответствии с правилами переходов. Необходимо отметить, что счетчиковая машина имеет всего лишь одно (детерминированное) исполнение из начальной конфигурации % так как каждое состояние имеет не более одного правила переходов. Машина Минского останавливается, если исполнение содержит конфигурацию с состоянием т.е. достигает финального состояния.
Говорят, что машина Минского ограничена при некоторой начальной конфигурации тогда и только тогда, когда существует натуральное число с', такое, что на протяжении всего исполнения машины из начальной конфигурации выполняется условие х1 + х2 + ... + хт < с', т.е. в любой момент времени сумма значений счетчиков не превосходит с'.
Машина Минского М тотально ограничена, если и только если она ограничена для всех возможных начальных конфигураций.
Теорема 1. Проблема ограниченности трехсчетчиковых машин Минского неразрешима.
Теорема 2. Для любой трехсчетчиковой машины Минского 3сМ может быть построена эквивалентная (имитирующая ее работу) машина Минского с двумя счетчиками 2сМ, такая, что конфигурация со значениями счетчиков у1 = = 2а • 3Ь • 5с и у2 = 0 машины 2сМ будет существовать тогда и только тогда, когда существует конфигурация с х1 = а, х2 = Ь и х3 = с машины 3сМ.
Замечания по теореме 2. Основная идея доказательства теоремы была взята из доказательства оригинальной теоремы М. Минского о моделировании трехсчетчиковой машины машиной с двумя счетчиками [5]. Однако в доказательстве оригинальной теоремы для двух машин 2сМ и 3сМ не обеспечивалась взаимная однозначность конфигураций со значениями счетчиков у1 = 2а • 3Ь • 5с, у2 = 0 и х1 = а, х2 = Ь, х3 = с соответственно. Потребовалось изменить конструкции моделирования таким образом, чтобы все вспомогательные переходы порождали конфигурации со значением у2 > 0. Как только значение счетчика у2 становится нулевым, это означает, что у1 содержит новое значение 2а • 3Ь • 5с, соответствующее х1 = а', х2 = Ь', х3 = с'. Вычисление же этого нового значения 2а • 3Ь • 5с начинается с увеличения нулевого значения у2 на единицу. Таким образом, конструкции, применяемые при доказательстве теоремы 2, обеспечивают для машин 2сМ и 3сМ взаимную однозначность конфигураций указанного вида, что позволяет использовать это утверждение для доказательства неразрешимости проблем, связанных также и с достижимостью конфигураций.
Теорема 3. Проблема ограниченности двух-счетчиковых машин Минского неразрешима.
Заметим, что из теоремы 2 также следует неразрешимость проблемы ограниченности одного счетчика двухсчетчиковой машины Минского, так как счетчик у1 машины 2сМ, содержащий значение 2 • 3 • 5 , где х1, х2 и х3 - счетчики машины 3сМ, будет ограничен тогда и только тогда, когда ограничена машина 3сМ. Таким образом, справедлива следующая
Теорема 4. Проблема ограниченности одного счетчика для двухсчетчиковых машин Минского не является разрешимой.
Замечания по теореме 3. Очевидно, что проблема ограниченности двухсчетчиковых машин Минского является частично разрешимой. Если машина 2сМ ограничена, то она будет иметь конечное множество всех возможных конфигураций. Таким образом, бесконечное исполнение машины (если оно существует) обязательно будет проходить одни и те же конфигурации. Следовательно, если после запуска машины 2сМ она попадет в конфигурацию, в которой уже находилась ранее (на исполнении), это и будет означать ограниченность машины, так как, начиная с данной конфигурации, будет порождаться бесконечный цикл, целиком состоящий из уже пройденных конфигураций, т.е. далее в исполнении новые конфигурации порождаться не будут.
Поскольку преобразования, используемые в доказательстве теоремы 2, исключают запуск машины 2сМ из нулевой начальной конфигурации, докажем неразрешимость и проблемы ограниченности двухсчетчиковых машин Минского для нулевой начальной конфигурации.
Теорема 5. Проблема ограниченности двухсчетчиковых машин Минского с нулевой начальной конфигурацией неразрешима.
Рассмотрим теперь двойственную к проблеме ограниченности (соответственно при нулевой конфигурации) задачу существования неограниченного исполнения (из нулевой конфигурации) двухсчетчиковой машины Минского. Перефразировав известную теорему Поста (см., например, в [3]), можно утверждать, что если проблема и ее дополнение (двойственная проблема) являются частично разрешимыми, следовательно, они обе разрешимы. А поскольку проблема ограниченности (как и проблема ограниченности для нулевой начальной конфигурации) является частично разрешимой, то получаем, что проблема неограниченного пути не может быть частично разрешимой. Таким образом, справедлива следующая
Теорема 6. Для двухсчетчиковых машин Минского (с нулевой начальной конфигурацией) проблема неограниченного пути не является частично разрешимой.
ПРОБЛЕМЫ ОГРАНИЧЕННОСТИ
743
Теорема 7. Для двухсчетчиковых машин Минского проблема тотальной ограниченности не является частично разрешимой.
Теорема 8. Проблема ограниченности хотя бы при одном входе для двухсчетчиковых машин Минского частично разрешима.
Теорема 9. Проблемы тотальной неограниченности и неограниченности хотя бы при одном входе для двухсчетчиковых машин Минского не являются частично разрешимыми.
ОГРАНИЧЕННОСТЬ ДЛЯ ОДНОСЧЕТЧИКОВОЙ МАШИНЫ МИНСКОГО
Пусть 1cM = (Q, {x}, А) - односчетчиковая машина Минского с начальной конфигурацией (q0, 0). Конечное исполнение машины 1cM обозначим п, а бесконечное - р = (q0, 0)(q1, n1)(q2, n2)(q3, n3), ..., где (q, n) - это i-я конфигурация исполнения р (г - номер текущей конфигурации в последовательности), qi - состояние из множества Q, а ni -значение счетчика x. Если машина 1cM имеет бесконечное исполнение р, будем писать ZERO(1cM) для обозначения множества номеров конфигураций исполнения р, в которых проверка на нуль прошла успешно, т.е. множество ZERO (1cM) будет состоять из номеров i конфигураций вида (q , 0), где qг - состояние второго типа:
ZERO(1cM) d= {0} и {i > 0: щ = щ + х = 0}.
Лемма 1 [8]. Пусть машина Минского 1cM имеет бесконечное исполнение р. Выберем элементы i < j множества ZERO(1cM), для которых не существует такого k е ZERO(1cM), что i < к < j.
Тогда будет выполняться неравенство
(j - i) <
\Q\2
Лемма 2 [8]. Пусть маш
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.