## From *Pre*historic to *Post*modern Symbolic Model Checking

*
Thomas A. Henzinger, Orna Kupferman, and Shaz Qadeer*

Symbolic model checking, which enables the automatic verification of large
systems, proceeds by calculating with expressions that represent state sets.
Traditionally, symbolic model-checking tools are based on *backward*
state traversal; their basic operation is the function *pre*, which
given a set of states, returns the set of all predecessor states. This is
because specifiers usually employ formalisms with future-time modalities,
which are naturally evaluated by iterating applications of *pre*. It
has been recently shown experimentally that symbolic model checking can
perform significantly better if it is based, instead, on *forward* state
traversal; in this case, the basic operation is the function *post*,
which given a set of states, returns the set of all successor states. This
is because forward state traversal can ensure that only those parts of the
state space are explored which are reachable from an initial state and
relevant for satisfaction or violation of the specification; that is, errors
can be detected as soon as possible.

In this paper, we investigate which specifications can be checked by symbolic
forward state traversal. We formulate the problems of symbolic backward and
forward model checking by means of two mu-calculi. The *pre*-mu
calculus is based on the *pre* operation; the *post*-mu calculus,
on the *post* operation. These two mu-calculi induce query logics,
which augment fixpoint expressions with a boolean emptiness query. Using
query logics, we are able to relate and compare the symbolic backward and
forward approaches. In particular, we prove that all omega-regular
(linear-time) specifications can be expressed as *post*-mu queries, and
therefore checked using symbolic forward state traversal. On the other hand,
we show that there are simple branching-time specifications that cannot be
checked in this way.

*Formal Methods in System Design* 23:303-327, 2003.
A preliminary version appeared in the
*Proceedings of the
Tenth International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 1427,
Springer, 1998, pp. 195-206.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1998, 2003 Springer.