Automatic Construction of Complete Abstraction by Abstract Interpretation

Abstraction plays a fundamental role in combating state-space explosion in model checking. Firstly, we study how to abstract models of mu-calculus and derive abstractions that are sound, and apply them to abstracting Kripke structures. However, a lack of completeness in the abstract interpretation leads to spurious counterexamples in the abstract model checking. In order to eliminate spurious counterexamples, the paper describes a method for minimally making abstract interpretations complete, and this refined complete abstract domain always exists.