Pi is a temporal formula that is true of a behavior iff:

• x is initially equal to 0.
• Each step either increments x by 1 or else is a stuttering step that leaves x unchanged.
• There are infinitely many steps that increment x .