Invariant checking.

An important class of CTL formulas is invariants, i.e., formulas of the form $\mathbf{AG} \alpha$, where $\alpha$ is propositional formula. The semantics of this kind of formulas is that $\alpha$ is true in all reachable states. The computation of this kind of formulas is based on a fix-point characterization [12]:

$$\mathbf{AG} \alpha = \mathbf{gfp}_Z [\alpha \wedge \mathbf{AX} Z]$$

This approach is not very direct, and can be quite inefficient. If the set of reachable states has been previously computed, then an invariant can be simply checked by performing a test of set inclusion between the states represented by $\alpha$ and the set of reachable states:

$$\mathbf{Reachable}(\mathcal{I}) \subseteq \alpha$$

NUSMV offers the possibility of checking invariants using either this or the standard model checking technique. These functionalities are the same as in CMU SMV. Moreover NUSMV, w.r.t. CMU SMV, has a specialized routine for checking invariants on the fly. This is performed by verifying at each step k of the reachability analysis the following condition:

$$R_k(\ensuremath{\underline{x}} ) \subseteq \alpha$$

where $R_k(\ensuremath{\underline{x}} )$ is the set of states reachable in k or fewer steps. If this test fails, then the invariant is not verified, and a counterexample leading to a state not satisfying the property is provided.