О минимизации и проверке эквивалентности последовательных реагирующих систем

Конечные автоматы-преобразователи (трансдьюсеры) над полугруппами могут служить формальными моделями последовательных реагирующих программ. В отдельных случаях задачу верификацию таких программ можно свести к задачам минимизации и проверки эквивалентности. Для эффективного решения этих задач приходится налагать некоторые ограничения на полугруппы, над которыми работают трансдьюсеры. Минимизация трансдьюсеров проводится в три этапа: вначале для всех состояний трансдьюсера вычисляются наибольшие общие делители, затем трансдьюсер преобразуется к приведенной форме путем «вынесения» таких делителей, и в заключении к приведенному трансдьюсеру применяются методы минимизации конечных автоматов. Предложенный метод минимизации позволяет также проверять эквивалентность трансдьюсеров.