Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking

Abstract

The verification process of reactive systems in local model checking [2,9,28] and in explicit state model checking [14,16] 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 [8,24] and, in particular, symbolic model checking [6,23] can utilize compact representations of the state space, e.g. BDDs [5], 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 [2] that enables the use of BDDs but still is on­the­fly.

This research is sponsored by the Semiconductor Research Corporation (SRC) under Contract No. 98-DJ-294, and the National Science Foundation (NSF) under Grant No. CCR-9505472. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of SRC, NSF, or the United States Government.