CTL model checking of complex systems often suffers from the
state-explosion problem. Symbolic Guided Search can be used to avoid
difficult-to-represent sections of the state space and prevent state
explosion from occurring.
Symbolic Guided Search applies hints to guide the exploration of the
state space. In this way, the size of the BDDs involved in the
computation is controlled, and the truth of a property may be decided
before all states have been explored. In this talk, we show how hints
can be used in the computation of nested fixpoints. We show how to use
hints to obtain both underapproximations and overapproximations.
Approximation techniques help model checking in two distinct ways: On
the one hand, the validity of a property can often be established on a
simplified model of the system. On the other hand, we can
successively refine an abstraction to compute the exact result. This
method is often more efficient than computing the exact result
directly, because we can direct the search of the state space to avoid
large BDDs. This use of approximations is one of the salient features
of symbolic model checking.
Under- and overapproximations can be obtained using methods that can
be broadly classified into three groups: Changing the formula,
changing the model, or changing the computation. In this talk we
discuss the last two.