Multiple State and Single State Tableaux for Combining Local and Global Model Checking - Correct System Design: Recent Insights and Advances - page 156

Multiple State and Single State Tableaux for
Combining Local and Global Model Checking ?

Armin Biere 1 , Edmund M. Clarke 1 ; 2 , and Yunshan Zhu 1

1

Verysys Design Automation, Inc, 42707 Lawrence Place, Fremont, CA 94538
[e-mail], [e-mail]

2

Computer Science Department, Carnegie Mellon University
5000 Forbes Avenue, Pittsburgh, PA 15213, U.S.A
[e-mail]

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.

1 Introduction

Model Checking [8, 24] is a powerful technique for the verification of reactive sys-
tems. With the invention of symbolic model checking [6, 23] very large systems, with
more than 10 20 states, could be verified. However, it is often observed, that explicit state
model checkers [11] outperform symbolic model checkers, especially in the application
domain of asynchronous systems and communication protocols [12]. We believe that
the main reasons are the following: First, symbolic model checkers traditionally use bi-
nary decision diagrams (BDDs) [5] as an underlying data structure. BDDs trade space
for time and often their sheer size explodes. Second, depth first search (DFS) is used
in explicit state model checking, while symbolic model checking usually traverses the
state space in breadth first search (BFS). DFS helps to reduce the space requirements
and is able to find counterexamples much faster. Finally, global model checking tra-
verses the state space backwards, and can, in general, not avoid visiting non reachable
states without a prior reachability analysis.

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