next up previous
Next: Invariant checking. Up: Advanced Functionalities Previous: Advanced Functionalities

Bounded CTL.

NUSMV allows expressing specifications in real-time CTL (RTCTL) [33]. For example, it is possible to express that $\alpha$ always leads to $\beta$ in 0 to 4 time units with the RTCTL specification10:

\begin{displaymath}\mathbf{AG} ( \alpha \rightarrow \mathbf{AF}^{0..4} \beta)

It is assumed that a time unit corresponds to a step. This functionality is the same as in CMU SMV.

NuSMV <>