Temporal formulas

Temporal formulas may contain all of the usual expression operator of SMV, plus the temporal operators G, F, X and U. The meanings of these operators are as follows:

• X p is true at time $t$ if p is true at time $t + 1$.
• G p is true at time $t$ if p is true at all times $t'\geq t$.
• F p is true at time $t$ if p is true at some time $t'\geq t$.
• p U q is true at time $t$ if q is true at some time $t'\geq t$, and for all times $< t'$ but $\geq t$, p is true.

A temporal formula is true for a given execution of the program if it is true at the initial time ($t = 0$).