Geodesic
The application of adaptive symmetry reduction for LTL model checking
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 78-87.

Voir la notice de l'article provenant de la source Math-Net.Ru

Adaptive symmetry reduction is a technique which exploits the similarity of components 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 feasible pseudo-cycle via an accepting state of Buchi automaton instead of a cycle. We 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.
Keywords: model checking, LTL, symmetry. 
@article{MAIS_2010_17_4_a8,
     author = {I. V. Konnov and V. A. Zakharov},
     title = {The application of adaptive symmetry reduction for {LTL} model checking},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {78--87},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a8/}
}
TY  - JOUR
AU  - I. V. Konnov
AU  - V. A. Zakharov
TI  - The application of adaptive symmetry reduction for LTL model checking
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 78
EP  - 87
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a8/
LA  - ru
ID  - MAIS_2010_17_4_a8
ER  - 
%0 Journal Article
%A I. V. Konnov
%A V. A. Zakharov
%T The application of adaptive symmetry reduction for LTL model checking
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 78-87
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a8/
%G ru
%F MAIS_2010_17_4_a8
I. V. Konnov; V. A. Zakharov. The application of adaptive symmetry reduction for LTL model checking. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 78-87. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a8/

[1] D. Bosnacki, “Nested depth first search algorithm for model checking with symmetry reduction”, Proceedings of FORTE 2002, Lecture Notes in Computer Science, 2529, 2002, 65–80 | Zbl

[2] M. C. Browne, E. M. Clarke, O. Grumberg, “Reasoning about networks with many identical finite-state processes”, Information and Computation, 81:1 (1989), 13–31 | DOI | MR | Zbl

[3] E. M. Clarke, O. Grumberg, O. E. Long, “Model checking and abstraction”, ACM Transactions on Programming Languages and Systems, 16:5 (1994), 1512–1542 | DOI

[4] E. M. Klark, O. Gramberg, D. Peled, Verifikatsiya modelei programm: Model Checking, Izd-vo MTsNMO, M., 2002, 416 pp.

[5] C. Courcoubetis, M. Y. Vardi, P. Wolper, M. Yannakakis, “Memory efficient algorithms for the verification of temporal properties”, Formal Methods in System Design, 1 (1992), 275–288 | DOI | MR

[6] E. A. Emerson, A. P. Sistla, “Symmetry and model checking”, Proceedings of the 5-nd Workshop on Computer-Aided Verification 1993, Lecture Notes in Computer Science, 697, 1993, 463–478 | MR

[7] R. Gerth, D. Peled, M. Vardi, P. Wolper, “Simple on-the-fly automatic verification of linear temporal logic”, Protocol Specification Testing and Verification, 1995, 3–18, Warsaw, Poland

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

[9] T. Wahl, “Adaptive symmetry reduction”, Proceedings of Computer Aided Verification 2007, Lecture Notes in Computer Science, 4590, 2007, 393–405 | Zbl