State focusing: Lazy abstraction for the Mu-calculus

A key technique for the verification of programs is counterexample-guided abstraction refinement (CEGAR). In a previous approach, we developed a CEGAR-based algorithm for the modal mu-calculus, where refinement applies only locally, i.e. lazy abstraction techniques are used. Unfortunately, our previous algorithm was not completely lazy and had some further drawbacks, like a possible local state explosion. In this paper, we present an improved algorithm that maintains all advantages of our previous algorithm but eliminates all its drawbacks. The improvements were only possible by changing the philosophy of refinement from state splitting into the new philosophy of state focusing, where the states that are about to be split are not removed.