|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного временистатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАК- Авторы: Гнатенко А.Р., Захаров В.А.
- Журнал: Моделирование и анализ информационных систем
- Том: 28
- Номер: 4
- Год издания: 2021
- Издательство: Яросл. гос. ун-т
- Местоположение издательства: Ярославль
- Первая страница: 378
- Последняя страница: 393
- DOI: 10.18255/1818-1015-2021-4-378-393
- Аннотация: К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, представляющих собой расширение темпоральных логик LTL, CTL и CTL* за счет использования регулярных языков в качестве параметров темпоральных операторов. Мы провели сравнительный анализ выразительных возможностей нового расширения темпоральной логики линейного времени Reg-LTL и предложили алгоритмы верификации моделей для новых расширений логик Reg-LTL, Reg-CTL, и Reg-CTL*. Однако вопрос о сложности задач верификации моделей и проверки выполнимости формул указанных логик оставался открытым. В этой статье мы восполняем этот пробел в наших исследованиях и показываем, что для темпоральной логики Reg-LTL обе задачи являются Pspace-полными. Вычислительная трудность рассматриваемых задач легко доказывается сведением к ним проблемы пустоты пересечения семейств регулярных языков. Основным результатом статьи является алгоритм сведения задачи проверкивыполнимости формул логики Reg-LTL к проблеме пустоты автоматов Бюхи сравнительно небольшого размера и описание стратегии, позволяющей проверять пустоту полученных автоматов с использованием объема памяти, полиномального относительно размера исходных формул.
- Добавил в систему: Захаров Владимир Анатольевич