Methods to Tackle State Explosion Problem in Model Checking

Abstract

Model checking is an automatic verification technique for finite state concurrent systems. In this approach to verification, temporal logic specifications are checked by an exhaustive search of the state space of the concurrent system. The size of the state space grows exponentially with the number of processes. This phenomenon is commonly called ¿State Explosion Problem¿. Many progress has been made on this problem. The main techniques can be classified into three types (1) based on automata theory, such as on-the-fly technique, partial order reduction technique etc. (2) based on symbolic structure, such as bounded model checking, SAT bounded model checking etc. (3) other methods such as abstraction, Symmetry, Compositional Reasoning etc. The aim of this paper is to give a succinct survey of methods to tackle State Explosion Problem in Model Checking.