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
,
is:

where

is the vector of state variables, is the transition relation and is the set of states reached in

The computation of the states reachable in *k*+1 steps can
be performed by considering only the frontier set
^{8}:

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.

NuSMV <>