Go backward to The Enabled Predicate Go up to Top Go forward to Temporal Formulas

Simple Temporal Logic

Execution of algorithm

• Sequence of steps.
• Each step produces new state changing the values of variables.
• Execution is sequence of states.
• Semantic meaning of algorithm is collection of all possible executions.

Temporal logic allows reasoning about sequences of states.