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 specification¹⁰:

$$\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.