Reachability-Guided Abstraction Refinement

Abstract To mitigate the state explosion problem in model checking, abstraction techniques provide sound but typically incomplete approximations of a system’s behaviour. While complete abstractions eliminate false alarms, they are often impractical—or even uncomputable—due to their high computational cost. We introduce semi-completeness, a relaxed notion of completeness that retains sufficient precision to capture a system’s behaviour over relevant regions of the domain. Building on this, we develop abstraction refinement algorithms that compute semi-complete abstractions without incurring the cost of full completeness. Furthermore, we present an algorithm that interleaves abstraction refinement with fixed-point computations—specifically reachability analysis. This achieves semi-completeness on-the-fly, without requiring prior knowledge of the region of interest, such as the reachable states. We demonstrate the effectiveness of our approach on fragments of the $\mu$ μ -calculus, showing that our abstractions preserve the validity of formulae over all reachable states.