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.
展开▼
