The application of adaptive symmetry reduction for LTL model checking
Abstract
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.
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.
About the Authors
I. V. Konnov
Московский государственный университет им. М.В. Ломоносова
Russian Federation
Russian Federation
V. A. Zakharov
Московский государственный университет им. М.В. Ломоносова
Russian Federation
Russian Federation
References
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
Review
For citations:
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.)
Views:
651
Email this article 