|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
Верификация моделей реагирующих систем относительно одного расширения темпоральной логики CTL*статья
- Авторы: Гнатенко А.Р., Захаров В.А.
- Сборник: Материалы XIII Международного семинара «Дискретная математика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.)
- Год издания: 2019
- Место издания: Изд-во механико-математического факультета МГУ
- Первая страница: 263
- Последняя страница: 266
- Аннотация: Язык LTL, хотя и вполне достаточный для большинства практических приложений, уступает по выразительным возможностям монадической логике 2-го порядка S1S. В разные годы предпринимались многократные попытки восполнить образовавшийся разрыв путем построения различных расширений LTL. Эти исследования были мотивированы, как правило, математическими соображениями. Однако недостаточные выразительные возможности LTL проявляются, в частности, при ее применении для спецификации вычислений систем обработки потоковых данных (реагирующих систем). Поведение таких систем проявляется в соответствии между потоками входных данных (показаний датчиков, управляющих сигналов) и выходных данных (команд, действий). В этом случае для описания потоков данных и команд целесообразно использовать теоретико-языковые средства (автоматы, грамматики, регулярные выражения), а для описания соответствия между этими потоками выгодно применять параметризованные темпоральные операторы. Ранее были описаны новое расширение логики линейного времени LP-LTL и алгоритм верификации моделей реагирующих систем относительно спецификаций, представленных формулами этой логики, а также было установлено, что LP-LTL и S1S имеют равные выразительные возможности. Открытыми оставались вопросы об объединении двух новых вариантов темпоральных логик и о сложности задачи верификации моделей реагирующих систем относительно расширенной параметризованной темпоральной логики LP-CTL*. В данной статье представлено решение обеих задач.
- Добавил в систему: Захаров Владимир Анатольевич