** Next:** LTL model checking.
** Up:** Advanced Functionalities
** Previous:** Invariant checking.

In NUSMV it is possible to compute quantitative information on the
Kripke structure [14,15]. In particular, it is possible
to compute the exact bound on the delay between two specified events,
expressed as CTL formulas:

The
computes the set of
states reachable from .
When a state satisfying
is
encountered, we return the number of steps taken so far. If a fixed
point is reached and no state satisfying
is found, then
*infinity* is returned.
has the dual interpretation, and
returns the length of the longest path from a state in
to a
state in .
If there exists an infinite path beginning in a
state in
that never reaches a state in ,
then
*infinity* is returned. This functionality is the same as in
CMU SMV.

NuSMV <>