Next: Quantitative characteristics computation.
Up: Advanced Functionalities
Previous: Bounded CTL.
An important class of CTL formulas is invariants,
i.e., formulas of the form
propositional formula. The semantics of this kind of formulas is that
is true in all reachable states. The computation of this kind
of formulas is based on a fix-point characterization :
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
and the set of reachable
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
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