О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени

Моделирование и анализ информационных систем. 2021. Т. 28. № 4. С. 356–371.

Гнатенко А. Р., Захаров В. А.

К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, представляющих собой расширение темпоральных логик LTL, CTL и CTL∗ за счет использования регулярных языков в качестве параметров темпоральных операторов. Мы провели сравнительный анализ выразительных возможностей нового расширения темпоральной логики линейного времени Reg-LTL и предложили алгоритмы верификации моделей для новых расширений логик Reg-LTL, Reg-CTL, и Reg-CTL∗. Однако вопрос о сложности задач верификации моделей и проверки выполнимости формул указанных логик оставался открытым. В этой статье мы восполняем этот пробел в наших исследованиях и показываем, что для темпоральной логики Reg-LTL обе задачи являются Pspace-полными. Вычислительная трудность рассматриваемых задач легко доказывается сведением к ним проблемы пустоты пересечения семейств регулярных языков. Основным результатом статьи является алгоритм сведения задачи проверки выполнимости формул логики Reg-LTL к проблеме пустоты автоматов Бюхи сравнительно небольшого размера и описание стратегии, позволяющей проверять пустоту полученных автоматов с использованием объема памяти, полиномального относительно размера исходных формул.

Ключевые слова: model checking, finite state transducer, конечный автомат-преобразователь, автомат Бюхи, верификация моделей программ, темпоральные логики, regular language, регулярный язык, Buchi automaton, Satisfiability problem, temporal logic

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