Incremental CTL Model Checking Using BDD Subsetting
Abelardo Pardo and Gary Hachtel
Proceedings of the Design Automation Conference, San Francisco, CA, 1998
Abstract
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. Both the
refinement and the abstraction procedures are based in BDD-subsetting.
Click here to download the compressed
postscript version.
BibTeX Entry
@InProceedings{Pardo98,
author = {A. Pardo and G. Hachtel},
title = {Incremental {CTL} Model Checking Using {BDD} Subsetting},
booktitle = "Proceedings of the Design Automation Conference",
year = 1998,
address = {San Francisco, CA},
month = jun,
% pages = {}
}
Return to the home page