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

Полный текст:


Аннотация

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

Об авторах

И. В. Коннов
Московский государственный университет им. М.В. Ломоносова
Россия


В. А. Захаров
Московский государственный университет им. М.В. Ломоносова
Россия


Список литературы

1. Bosnaeki D, Nested depth first search algorithm for model checking with symmetry reduction // Proceedings of FORTE 2002, 2002, Lecture Notes in Computer Science, V. 2529/2002. P. 65-80.

2. Browne M.C., Clarke E.M., Grumberg O. Reasoning about networks with many identical finite-state processes // Information and Computation. 1989. 81(1). P. 13-31.

3. Clarke E.M., Grumberg O,, Long O.E. Model checking and abstraction // ACM Transactions on Programming Languages and Systems. 1994. V. 16, N 5. P. 1512-1542.

4. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: Изд-во МЦНМО, 2002. 416 с.

5. Coureoubetis С., Vardi M.Y., Wolper P., Yannakakis M. Memory efficient algorithms for the verification of temporal properties // Formal Methods in System Design. 1992. V. 1. P. 275-288.

6. Emerson E.A., Sistla A.P. Symmetry and model checking j j Proceedings of the 5-nd Workshop on Computer-Aided Verification 1993, 1993, Lecture Notes in Computer Science. V. 697/1993. P. 463-478.

7. Gerth Е,, Peled D,, Vardi М.. and Wolper P. Simple on-the-flv automatic verification of linear temporal logic // Protocol Specification Testing and Verification. Warsaw, Poland, 1995, P. 3-18

8. Godefroid P. Using Partial orders to improve automatic verification methods. Proceedings of the 2-nd Workshop on Computer-Aided Verification. ACM Transactions on Programming Languages and Systems, 1990, Lecture Notes in Computer Science, V, 531/1990, P. 176-185

9. Wahl T, Adaptive symmetry reduction. Proceedings of Computer Aided Verification 2007, Lecture Notes in Computer Science. V. 4590/2007. P. 393-405


Дополнительные файлы

Для цитирования: Коннов И.В., Захаров В.А. Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени. Моделирование и анализ информационных систем. 2010;17(4):78-87.

For citation: Konnov I.V., Zakharov V.A. The application of adaptive symmetry reduction for LTL model checking. Modeling and Analysis of Information Systems. 2010;17(4):78-87. (In Russ.)

Просмотров: 7

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)