Incremental CTL model checking using BDD subsetting
Abelardo Pardo, Gary D. Hachtel · 1998
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 existen tial fragments. The algorithm begins with conserv ativ everification of an initial abstraction. If the conclusion is negativ e,it deriv es a “goal set” of states which require further resolution. It then successiv ely refines, with respect to this goal set, the appro ximations made in the sub-formulas, until the giv en form ula is v erified or computational resources are exhausted. This method applies uniformly to the abstractions based in over-appro ximation 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-appro ximation on the universal fragment (or for language con tainment), whereas the goal set method is applicable to all consisten t appro ximations, and for all CTL formulas.