Next: Fair CTL model checking.
Up: Standard Functionalities
NUSMV, (similarly to CMU SMV), offers an enhanced algorithm for
reachability analysis. The standard way to perform the
computation of the reachable states
starting from the initial states
where k is the minimum integer such that
is recursively defined as:
is the vector of state variables,
transition relation and
is the set of states reached in
k or fewer steps.
The computation of the states reachable in k+1 steps can
be performed by considering only the frontier set
We are planning to introduce new optimizations to the computation of the set
of reachable states, such as the use of don't care sets. The set of reachable
states can be used to simplify the following model checking computations.