Systematic Construction of Abstractions for Model-Checking
Abstract
This paper describes a framework, based on Abstract Interpretation,
for creating abstractions for model-checking. Specifically, we
study how to abstract models of $\mu$-calculus
and systematically derive abstractions that
are constructive, sound, and precise, and apply them to
abstracting Kripke structures. The overall approach is based on the use of
bilattices to represent partial and inconsistent information.