Making Abstraction Refinement Efficient in Model Checking

TL;DR

This paper introduces a novel abstraction refinement method for model checking that adds extra variables to avoid NP-hard state separation, resulting in smaller refined models and improved efficiency.

Contribution

The paper proposes a new refinement technique that bypasses NP-hard problems by adding extra variables, enhancing the efficiency of model checking.

Findings

Avoids NP-hard state separation problem

Produces smaller refined abstract models

Improves efficiency of abstraction refinement

Abstract

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, although the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. And 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 by adding extra variables to the abstract model for the refinement. With this method, not only the NP-hard state separation problem is avoided, but also a smaller refined abstract model is obtained.