Combining local and global model checking

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.