Making Abstraction-Refinement Efficient in Model Checking

摘要

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the 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 method is presented, in which extra variables are added to the abstract model for the refinement. With this method, not only the NP-hard state separation problem can be avoided, but also a smaller refined abstract model can be obtained.