Combining search space partition and abstraction for LTL model checking

The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the integration of search space partition and abstraction improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.