KIT | KIT-Bibliothek | Impressum | Datenschutz

Combining local and global model checking

Biere, Armin; Clarke, Edmund M.; Zhu, Yunshan

Abstract:

The verification process of reactive systems in local model
checking
[BhatCleavelandGrumberg95,Cleaveland90,StirlingWalker91] and in
explicit state model checking
[GerthPeledVardiWolper95,Holzmann97] is
on-the-fly. Therefore only those states of a system have to be
traversed that are necessary to prove a property. In addition,
if the
property does not hold, than often only a small subset of the
state
space has to be traversed to produce a counterexample. Global
model
checking [ClarkeEmerson81,QuielleSifakis81] and, in particular,
symbolic model checking [BurchClarkeMcMillan92,McMillan93] can
utilize
compact representations of the state space, e.g. BDDs
[Bryant86], to
handle much larger designs than what is possible with local and
explicit model checking. We present a new model checking
algorithm for
LTL that combines both approaches. In essence, it is a
generalization
of the tableau construction of [BhatCleavelandGrumberg95] that
enables
the use of BDDs but still is on-the-fly.


Volltext §
DOI: 10.5445/IR/48399
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 1999
Sprache Englisch
Identifikator ISSN: 1432-7864
urn:nbn:de:swb:90-AAA483992
KITopen-ID: 48399
Verlag Universität Karlsruhe (TH)
Serie Interner Bericht. Fakultät für Informatik, Universität Karlsruhe ; 1998,26
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page