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

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