Quantitative characteristics computation.

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:

$$\begin{array}{c@{\hspace{1cm}}c} \textbf{MIN} [ \alpha, \beta ] & \textbf{MAX} [ \alpha, \beta ] \end{array}$$

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