2. 2. state explosion Problem
State explosion is the major problem in model checking.
The number of global states of a concurrent system with
many processes can be enormous. It is easy to see why this
is true. The asynchronous composition of n processes,
each having m states, may have mn states. A similar problem occurs with data. The state-transition system for an
n-bit counter will have 2n states. All model checkers suffer from this problem. Complexity-theoretic arguments
can be used to show that the problem is unavoidable in
the worst case (assuming P is different than PSPACE).
Fortunately, steady progress has been made over the past
28 years for special types of systems that occur frequently
in practice. In fact, the state explosion problem has been
the driving force behind much of the research in model
checking and the development of new model checkers. We discuss below key breakthroughs that have been
made and some of the important cases where additional
research is needed.
2. 3. major Breakthroughs
2. 3. 1. Symbolic Model Checking with OBDDs. In the original implementation of the model checking algorithm, transition relations were represented explicitly by adjacency
lists.
11 For concurrent systems with small numbers of processes, the number of states was usually fairly small, and the
approach was often quite practical. In systems with many
concurrent parts the number of states in the global state-transition system was too large to handle. In the fall of 1987,
McMillan, then a graduate student at Carnegie Mellon, realized that by using a symbolic representation for the state-transition systems, much larger systems could be verified.
The new symbolic representation was based on Bryant’s
ordered binary decision diagrams (OBDDs). OBDDs provide a
canonical form for Boolean formulas that is often substantially more compact than conjunctive or disjunctive normal
form, and very efficient algorithms have been developed for
manipulating them. Because the symbolic representation
captures some of the regularity in the state space determined
by circuits and protocols, it is possible to verify systems with
an extremely large number of states—many orders of magnitude larger than could be handled by the explicit-state algorithms. With the new representation for state-transition
systems, we could verify some examples that had more than
1020 states.
8, 35 Since then, various refinements of the OBDD-based techniques have pushed the state count up to more
than 10120.
2. 3. 2. Partial Order Reduction. Verifying software poses
significant problems for model checking. Software tends to
be less structured than hardware. In addition, concurrent
software is usually asynchronous, i.e., most of the activities
taken by different processes are performed independently,
without a global synchronizing clock. For these reasons,
the state explosion problem is particularly serious for software. Consequently, model checking has been used less
frequently for software verification than for hardware verification. One of the most successful techniques for dealing
with asynchronous systems is the partial order reduction.
This technique exploits the independence of concurrently
executed events. Intuitively, two events are independent of
each other when executing them in either order results in
the same global state. In this case, it is possible to avoid exploring certain paths in the state-transition system. Model
checking algorithms that incorporate the partial order
reduction are described in several different papers. The
stubborn sets of Valmari,
45 the persistent sets of Godefroid27
and the ample sets of Peled,
38 differ on the actual details,
but contain many similar ideas. The SPIN model checker
developed by Holzmann uses the ample-set reduction to
great advantage.
2. 3. 3. Bounded Model Checking with SAT. Although symbolic model checking with OBDDs was the first big breakthrough on the state explosion problem and is still widely
used, OBDDs have a number of problems that limit the
size of the models that can be checked with this technique. The ordering of variables on each path from the
root of the OBDD to a leaf has to be the same. Finding an
ordering that results in a small OBDD is quite difficult. In
fact, for some Boolean formulas no space-efficient ordering is possible. A simple example is the formula for the
middle output bit of a combinational multiplier for two
n-bit numbers. It is possible to prove that the OBDD for
this formula has size that is exponential in n for all variable orderings.
Propositional satisfiability (SAT) is the problem of determining whether a propositional formula in conjunctive normal form (“product of sums form” for Boolean formulas) has
a truth assignment that makes the formula true. The problem is NP-complete (in fact, it is usually the first example
of this class that students see). Nevertheless, the increase
in power of modern SAT solvers over the past 15 years on
problems that occur in practice has been phenomenal. It
has become the key enabling technology in applications of
model checking to both computer hardware and software.
Bounded Model Checking (BMC) of computer hardware
using a fast SAT solver is now probably the most widely used
model checking technique. The counterexamples that it
finds are just the satisfying instances of the propositional
formula obtained by unwinding to some fixed depth the
state-transition system for the circuit and the negation of its
specification in linear TL.
The basic idea for BMC is quite simple (cf. Biere et al.
7).
The extension to full LTL obscures the simplicity so we will
just describe how to check properties of the form FP where
the property P is an atomic proposition (e.g., “Message_
Received”). BMC determines whether there is a counterexample of length k (we assume k ³
1). In other words,
it checks if there is a path of length k ending in a cycle in
which each state is labeled with ¬ P (see Figure 3). Assume
that the state-transition system M has n states. Each state
can be encoded by a vector v of élog(n)ù Boolean variables.
figure 3. counterexample of length at most k.
¬p
s0 sk
¬p
s1 s2
¬p ¬p
sk– 2 sk– 1