Go to the first, previous, next, last section, table of contents.
The specifications to be checked on the Kripke structure can be expressed in the temporal logics CTL and LTL. Furthermore, it is possible to analyze quantitative characteristics of the model by specifying computations. Specifications can be positioned within modules. The specification is processed in such a way to rename the variables according to the containing context.
Specifications are evaluated by NuSMV. In case of a CTL or LTL
false specification, a counterexample is printed out.