Automatic abstraction techniques for propositional μ-calculus model checking

Abstract

An abstraction/refinement paradigm for the full propositional μ-calculus is presented. No distinction is made between universal or existential fragments. Necessary conditions for conservative verification are provided, along with a fully automatic symbolic model checking abstraction algorithm. The algorithm begins with conservative verification of an initial abstraction. If the conclusion is negative, it derives a "goal set" of states which require further resolution. It then successively refines, with respect to this goal set, the approximations made in the sub-formulas, until the given formula is verified or computational resources are exhausted.