The application of adaptive symmetry reduction for LTL model checking

• Main Authors: I. V. Konnov, V. A. Zakharov
• Format: Article
• Language: English
• Published: Yaroslavl State University 2010-12-01
• Series: Modelirovanie i Analiz Informacionnyh Sistem
• Subjects: model checking; ltl; symmetry
• Online Access: https://www.mais-journal.ru/jour/article/view/1054

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.