Partition Refinement in Abstract Model Checking

Model checking has been successfully applied to system verification. However, in model checking, the state explosion problem occurs when one checks systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper describes a technique to decompose a model checking problem into sub-problems by partitioning the search space. The partitioning is based on the usage of extra variables remembering the history of non-deterministic choices in the model. Furthermore, the search space can be partitioned stepwise in order to get better reduction. Finally, the partition-refinement paradigm is extended to the setting of abstract systems. We show how the partition-based approach used in abstract model checking can improve the efficiency of verification with respect to the requirement of memory by illustrating an application example.