Моделирование и анализ поведения последовательных реагирующих программ

Труды Института системного программирования РАН. 2015. Т. 27. № 2. С. 221–250.

Захаров В. А.

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

Ключевые слова: полугруппа, complexity, semigroup, алгоритмическая сложность, reactive program, finite state transducer, equivalence checking, decision procedure, реагирующая программа, конечный автомат-преобразователь, проверка эквивалентности, разрешающая процедура

ПУБЛИКАЦИЯ ПОДГОТОВЛЕНА ПО РЕЗУЛЬТАТАМ ПРОЕКТА: Моделирование, анализ и улучшение качества процессов в информационных системах (2015)