Abstraction-Based Model Checking Using Modal Transition Systems

We present a framework for automatic program abstraction that can be used for model checking any formula of the modal mu-calculus. Unlike traditional "conservative" abstraction which can only prove universal properties, our framework can both prove and disprove algorithms for automatically generating an abstract "modal transition system" (MTS) by adapting existing predicate and cartesian abstraction techniques. We show that model-checking of arbitrary formulas using abstract MTSs can be done at the same cost as conservative abstraction for universal formulas.