From Pre-historic to Post-modern Symbolic Model Checking.
========================================================
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
{\em 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 {\em 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 \premu calculus is based on the $\pre$ operation;
the \postmu 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 \postmu 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.