maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1054Research ArticleОригинальные статьиArticlesАдаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времениThe application of adaptive symmetry reduction for LTL model checkingКонновИ. В.KonnovI. V.konnov@cs.msu.suЗахаровВ. А.ZakharovV. A.zakh@cs.msu.suМосковский государственный университет им. М.В. ЛомоносоваRussian Federation2010201220101747887Copyright © Коннов И.В., Захаров В.А., 20102010Коннов И.В., Захаров В.А.Konnov I.V., Zakharov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1054

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

Adaptive symmetry reduction is a technique which exploits the similarity of com- ponents in systems of regular structure. It helps to reduce the effect of state explosion when exploring reachable states of a system. It assumes the perfect symmetry of states initially and tracks symmetry violations on-the-fly by exploring an extended state space. In this paper we show that the technique is applicable to LTL model checking as well. To succeed in this we incorporate the operations over the extended state space into the classic double depth-first search algorithm. The nested search is modified to detect a fea- sible pseudo-cycle via an accepting state of Buchi automaton instead of a cycleWe show that the existence of a pseudo-cycle results in satisfiability of an Indexed LTL formula on a model of the system and vice versa. This result opens the way for implementing adaptive symmetry reduction in a LTL model checker.

верификациялогика линейного временисимметрияmodel checkingLTLsymmetryReferencesBosnaeki 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.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.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.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.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.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.Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: Изд-во МЦНМО, 2002. 416 с.Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: Изд-во МЦНМО, 2002. 416 с.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.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.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.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.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-18Gerth Е,, 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-18Godefroid 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-185Godefroid 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-185Wahl T, Adaptive symmetry reduction. Proceedings of Computer Aided Verification 2007, Lecture Notes in Computer Science. V. 4590/2007. P. 393-405Wahl T, Adaptive symmetry reduction. Proceedings of Computer Aided Verification 2007, Lecture Notes in Computer Science. V. 4590/2007. P. 393-405

The authors declare that there are no conflicts of interest present.