The magic of symbolic model checking:
In symbolic model checking, instead of building a list of reachable
states, a predicate forumla, q(s), is constructed that is true iff s
is a reachable state.
The magic key to the efficiently finding the allowable states during
symbolic model checking can be explained as follows
\E (a, b, c, ...) . R(q', a, b, c, ...)
can be written as
\E(b, c, ...) . \E a . R(q', a, b, c, ...)
Therefore, instead of performing a search over the exponential set of
values defined by the state tupple (a, b, c, ...) we can instead use a
linear number of operations. Each operation removes a variable from s
and we end up with an explicit expression for q'.
However, we can go one better than that: the BDD implementation of `forsome'
(the existential quantifier) can easily be implemented to accept a list
of variables and to quantify over them all in one operation, and so even the
`linear' part is somewhat ameliorated.
In the above, R is the next state relation, q is the allowable states
predicate and the prime denotes the value in the next state.
The state itself, s, is the vector (a, b, c, ...).
DJ Greaves.