On the model checking of finite state transducers over semigroups

Последовательные реагирующие системы - это программы, которые взаимодействуют с окружением, получая от него сигналы или запросы, и реагируют на эти запросы, проводя операции с данными. Подобные системы могут служить моделью для многих программ: драйверов, систем реального времени, сетевых протоколов и др. В статье исследуются задача верификации программ такого вида. В качестве формальных моделей для реагирующих систем мы используем конечные автоматы-преобразователи, работающие над полугруппами. Для описания поведения автоматов-преобразователей введён новый язык спецификаций LP-CTL*. В его основу положена темпоральная логика CTL*. Этот язык спецификаций имеет две характерные особенности: 1) каждый темпоральный оператор снабжён регулярным выражением над входным алфавитом автомата, и 2) каждое атомарное высказывание задается регулярным выражением над выходным алфавитом автомата-преобразователя. В данной работе представлен табличный алгоритм проверки выполнимости формул LP-CTL* на моделях конечных автоматов-преобразователей, работающих над свободными полугруппами. Доказана корректность предложенного алгоритма и получена оценка его сложности. Кроме того, рассмотрен специальный фрагмент языка LP-CTL*, содержащий в качестве параметров темпоральных операторов только регулярные выражения над однобуквенным алфавитом. Показано, что этот фрагмента применим для спецификаций обычных моделей Крипке, и при этом его выразительные возможности превосходят обычную логику CTL*.