|
ИСТИНА |
Войти в систему Регистрация |
ФНКЦ РР |
||
О верификации конечных автоматов-преобразователей над полугруппамистатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАКДата последнего поиска статьи во внешних источниках: 16 января 2019 г.
- Авторы: Гнатенко А.Р., Захаров В.А.
- Журнал: Труды Института системного программирования РАН (электронный журнал)
- Том: 30
- Номер: 3
- Год издания: 2018
- Первая страница: 303
- Последняя страница: 324
- DOI: 10.15514/ISPRAS-2018-30(3)-21
- Аннотация: Последовательные реагирующие системы – это программы, которые взаимодействуют с окружением, получая от него сигналы или запросы, и реагируют на эти запросы, проводя операции с данными. Подобные системы могут служить моделью для многих программ: драйверов, систем реального времени, сетевых протоколов и др. В статье исследуются задача верификации программ такого вида. В качестве формальных моделей для реагирующих систем мы используем конечные автоматы-преобразователи, работающие над полугруппами. Для описания поведения автоматов-преобразователей введён новый язык спецификаций LP-CTL*. В его основу положена темпоральная логика CTL*. Этот язык спецификаций имеет две характерные особенности: 1) каждый темпоральный оператор снабжён регулярным выражением над входным алфавитом автомата, и 2) каждое атомарное высказывание задается регулярным выражением над выходным алфавитом автомата-преобразователя. В данной работе представлен табличный алгоритм проверки выполнимости формул LP-CTL* на моделях конечных автоматов-преобразователей, работающих над свободными полугруппами. Доказана корректность предложенного алгоритма и получена оценка его сложности. Кроме того, рассмотрен специальный фрагмент языка LP-CTL*, содержащий в качестве параметров темпоральных операторов только регулярные выражения над однобуквенным алфавитом. Показано, что этот фрагмента применим для спецификаций обычных моделей Крипке, и при этом его выразительные возможности превосходят обычную логику CTL*.
- Добавил в систему: Захаров Владимир Анатольевич