- Об институте
- Инновации
- Структура
- Отдел "Архитектуры вычислительных систем"
- Отдел "Информационных систем"
- Отдел "Компиляторных технологий"
- Отдел "Системного программирования"
- Отдел "Системной интеграции и прикладных программных комплексов"
- Отдел "Теоретической информатики"
- Отдел "Технологий программирования"
- Ученый совет
- Диссертационный совет
- Центр верификации ОС Linux
- Исследовательский центр доверенного искусственного интеллекта
- Центр компетенции по параллельным и распределенным вычислениям
- Образование
- Издания
- Новости
- Лицензии
Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени.
Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени.
Авторы
Захаров В.А., Коннов И.В.
Аннотация
Показано, что метод адаптивной редукции симметричных моделей (ASR), предложенный для сокращения пространства поиска при решении проблемы достижимости в моделях программ, может быть с равным успехом применен для проверки выполнимости формул логики линейного времени ILTL на конечных моделях распределённых программ. Задача проверки выполнимости формул ILTL сводится к задаче проверки пустоты автомата Бюхи, решаемой при помощи комбинированного алгоритма, в котором процедура двойного поиска в глубину (DDFS) сочетается с последовательным уточнением пространства поиска на основе принципов ASR.
Полный текст статьи в формате pdfКлючевые слова
верификация, логика линейного времени, симметрия
Издание
Моделирование и анализ информационных систем, 2010, том 17, № 4, с. 78-87.
Научная группа
Все публикации за 2010 год
