Dissemin is shutting down on January 1st, 2025

Published in

Proceedings 1998 Design and Automation Conference. 35th DAC. (Cat. No.98CH36175)

DOI: 10.1109/dac.1998.724515

Proceedings of the 35th annual conference on Design automation conference - DAC '98

DOI: 10.1145/277044.277171

Links

Tools

Export citation

Search in Google Scholar

Incremental CTL Model Checking Using BDD Subsetting

Journal article published in 1998 by Abelardo Pardo ORCID, Gary D. Hachtel
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Green circle
Postprint: archiving allowed
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

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. 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...