Linear-time Temporal Logic

Temporal logic is a convenient formalism for specifying and verifying properties of reactive systems, as first pointed out by Pnueli in 1977. A formula of temporal logic describes the set of infinite sequences for which it is true, also known as a temporal property . A given system satisfies a property if all of its computations belong to this set.

A model of linear-time temporal logic (LTL) is an infinite sequence of states where each point in time has a unique successor. Temporal formulas are evaluated over such a sequence of states together with an index i=0,1,2,... of the i'th state.

Syntax and informal description

Besides the usual logical connectives, temporal formulas can be composed using temporal operators. We describe these briefly, with p and q being sub-formulas.

Future Temporal Operators
[]p Henceforth p
<>p Eventually p
p Until q q holds some time in the future, and p holds at least up to the first q
p Awaits q Either p holds indefinitely, or p Until q
()p p holds at the next time instance


Past Temporal Operators
[-]p So-far p
<->p Once p
p Since q q did hold some time in the past, and p held at least down to the first q
p Backto q Either p Since q, or [-]p
(-)p p holds at the previous time instance (and current time is not 0)
(~)p p holds at the previous time instance or the current time is 0 (there is no previous time instance)

Semantics

A temporal logic formula p is satisfiable if there is a sequence of states S such that S,0 |= p. It is valid if the negation is unsatisfiable. A propositional temporal formula is a temporal formula where all atoms are propositional variables (a propositional temporal formula therefore does not contain quantification and compound predicates).
Last modified: Wed Jul 1 10:01:34 PDT 1998