Incremental CTL model checking using BDD subsetting

An automatic abstraction/refinement algorithm for symbolic CTL model checking is presented. Conservative model checking is thus done for the full CTL language-no restriction is made to the universal or existential fragments. 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. This method applies uniformly to the abstractions based in over-approximation as well as under-approximations of the model. Both the refinement and the abstraction procedures are based in BDD-subsetting. Note that refinement procedures which are based on error traces, are limited to over-approximation on the universal fragment (or for language containment), whereas the goal set method is applicable to all consistent approximations, and for all CTL formulas.