О минимизации и проверке эквивалентности последовательных реагирующих систем
Язык статьи
Английский
Аннотация
Конечные автоматы-преобразователи (трансдьюсеры) над полугруппами могут служить формальными моделями последовательных реагирующих программ. В отдельных случаях задачу верификацию таких программ можно свести к задачам минимизации и проверки эквивалентности. Для эффективного решения этих задач приходится налагать некоторые ограничения на полугруппы, над которыми работают трансдьюсеры. Минимизация трансдьюсеров проводится в три этапа: вначале для всех состояний трансдьюсера вычисляются наибольшие общие делители, затем трансдьюсер преобразуется к приведенной форме путем «вынесения» таких делителей, и в заключении к приведенному трансдьюсеру применяются методы минимизации конечных автоматов. Предложенный метод минимизации позволяет также проверять эквивалентность трансдьюсеров.
Ключевые слова
DOI
10.31144/si.2307-6410.2016.n7.p33-44
УДК
Страницы
33-44
Файл
zakharov-systinf.pdf100.83 КБ
Номер