Reachability Analysis.

NUSMV, (similarly to CMU SMV), offers an enhanced algorithm for reachability analysis. The standard way to perform the computation of the reachable states $\mathbf{Reachable}(\mathcal{I})$, starting from the initial states $\ \mathcal{I}$, is:

$$\mathbf{Reachable}(\mathcal{I}) = R_k(\ensuremath{\underline{x}} )$$

where k is the minimum integer such that $R_k(\ensuremath{\underline{x}} ) = R_{k+1}(\ensuremath{\underline{x}} )$, and $R_k(\ensuremath{\underline{x}} )$ is recursively defined as:

$$\begin{array}{lll} R_0(\ensuremath{\underline{x}} ) & = &\ma... ...rline{x}} '] \cup R_k(\ensuremath{\underline{x}} ) \end{array}$$

$\ensuremath{\underline{x}}$ is the vector of state variables, $T(\cdot,\cdot)$ is the transition relation and $R_k(\ensuremath{\underline{x}} )$ 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 $F_k(\ensuremath{\underline{x}} ) = R_k(\ensuremath{\underline{x}} )\wedge\overline{R_{k-1}(\ensuremath{\underline{x}} )}$⁸:

$$\begin{array}{lll} R_{k+1}(\ensuremath{\underline{x}} ) & = ... ...rline{x}} '] \cup R_k(\ensuremath{\underline{x}} ) \end{array}$$

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.