Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени.

Авторы

Захаров В.А., Коннов И.В.

Аннотация

Показано, что метод адаптивной редукции симметричных моделей (ASR), предложенный для сокращения пространства поиска при решении проблемы достижимости в моделях программ, может быть с равным успехом применен для проверки выполнимости формул логики линейного времени ILTL на конечных моделях распределённых программ. Задача проверки выполнимости формул ILTL сводится к задаче проверки пустоты автомата Бюхи, решаемой при помощи комбинированного алгоритма, в котором процедура двойного поиска в глубину (DDFS) сочетается с последовательным уточнением пространства поиска на основе принципов ASR.

Полный текст статьи в формате pdf

Ключевые слова

верификация, логика линейного времени, симметрия

Издание

Моделирование и анализ информационных систем, 2010, том 17, № 4, с. 78-87.

Научная группа

Теоретическая информатика

Все публикации за 2010 год

Все публикации