An efficient approach for abstraction-refinement in model checking

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In an abstract model, the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. Accordingly, the abstract model needs to be further refined where an NP-hard state separation problem is often involved. In this paper, a novel approach is presented, in which extra boolean variables are added to the abstract model for the refinement. With this approach, not only the NP-hard state separation problem can be avoided, but also a smaller refined abstract model can be obtained.