[Next] [Up] [Previous] [Contents]

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 .
• F p is true at time t if p is true at some time .
• p U q is true at time t if q is true at some time , and for all times < t' but , p is true.

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