In logic, linear temporal logic or linear-time temporal logic[1] [2] (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. LTL is sometimes called propositional temporal logic, abbreviated PTL.[3] In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.[4] [5]
LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.[6]
LTL is built up from a finite set of propositional variables AP, the logical operators ¬ and ∨, and the temporal modal operators X (some literature uses O or N) and U. Formally, the set of LTL formulas over AP is inductively defined as follows:
X is read as next and U is read as until.Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators, in order to write LTL formulas succinctly.The additional logical operators are ∧, →, ↔, true, and false.Following are the additional temporal operators.
An LTL formula can be satisfied by an infinite sequence of truth valuations of variables in AP.These sequences can be viewed as a word on a path of a Kripke structure (an ω-word over alphabet 2AP).Let w = a0,a1,a2,... be such an ω-word. Let w(i) = ai. Let wi = ai,ai+1,..., which is a suffix of w. Formally, the satisfaction relation ⊨ between a word and an LTL formula is defined as follows:
We say an ω-word w satisfies an LTL formula when w ⊨ . The ω-language L defined by is, which is the set of ω-words that satisfy .A formula is satisfiable if there exist an ω-word w such that w ⊨ . A formula is valid if for each ω-word w over alphabet 2AP, we have w ⊨ .
The additional logical operators are defined as follows:
The additional temporal operators R, F, and G are defined as follows:
Some authors also define a weak until binary operator, denoted W, with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release).[8] It is sometimes useful since both U and R can be defined in terms of the weak until:
The strong release binary operator, denoted M, is the dual of weak until. It is defined similar to the until operator, so that the release condition has to hold at some point. Therefore, it is stronger than the release operator.
The semantics for the temporal operators are pictorially presented as follows.
| Textual | Symbolic | Explanation | Diagram | |
|---|---|---|---|---|
| Unary operators | ||||
| X φ | circ\varphi | neXt: φ has to hold at the next state. | ||
| F φ | \Diamond\varphi | Finally: φ eventually has to hold (somewhere on the subsequent path). | ||
| G φ | \Box\varphi | Globally: φ has to hold on the entire subsequent path. | ||
| Binary operators: | ||||
| ψ U φ | \psi l{U}\varphi | Until: ψ has to hold at least until φ becomes true, which must hold at the current or a future position. | ||
| ψ R φ | \psi l{R}\varphi | Release: φ has to be true until and including the point where ψ first becomes true; if ψ never becomes true, φ must remain true forever. | ||
| ψ W φ | \psi l{W}\varphi | Weak until: ψ has to hold at least until φ; if φ never becomes true, ψ must remain true forever. | ||
| ψ M φ | \psi l{M}\varphi | Strong release: φ has to be true until and including the point where ψ first becomes true, which must hold at the current or a future position. | ||
Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators.
| Distributivity | |||
|---|---|---|---|
| X (φ ∨ ψ) ≡ (X φ) ∨ (X ψ) | X (φ ∧ ψ) ≡ (X φ) ∧ (X ψ) | X (φ U ψ)≡ (X φ) U (X ψ) | |
| F (φ ∨ ψ) ≡ (F φ) ∨ (F ψ) | G (φ ∧ ψ) ≡ (G φ) ∧ (G ψ) | ||
| ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ) | (φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ) | ||
| Negation propagation | ||||
|---|---|---|---|---|
| X is self-dual | F and G are dual | U and R are dual | W and M are dual | |
| ¬X φ ≡ X ¬φ | ¬F φ ≡ G ¬φ | ¬ (φ U ψ) ≡ (¬φ R ¬ψ) | ¬ (φ W ψ) ≡ (¬φ M ¬ψ) | |
| ¬G φ ≡ F ¬φ | ¬ (φ R ψ) ≡ (¬φ U ¬ψ) | ¬ (φ M ψ) ≡ (¬φ W ¬ψ) | ||
| Special temporal properties | |||
|---|---|---|---|
| F φ ≡ F F φ | G φ ≡ G G φ | φ U ψ ≡ φ U (φ U ψ) | |
| φ U ψ ≡ ψ ∨ (φ ∧ X(φ U ψ)) | φ W ψ ≡ ψ ∨ (φ ∧ X(φ W ψ)) | φ R ψ ≡ ψ ∧ (φ ∨ X(φ R ψ)) | |
| G φ ≡ φ ∧ X(G φ) | F φ ≡ φ ∨ X(F φ) | ||
All the formulas of LTL can be transformed into negation normal form, where
Using the above equivalences for negation propagation, it is possible to derive the normal form. This normal form allows R, true, false, and ∧ to appear in the formula, which are not fundamental operators of LTL. Note that the transformation to the negation normal form does not blow up the length of the formula. This normal form is useful in translation from an LTL formula to a Büchi automaton.
LTL can be shown to be equivalent to the monadic first-order logic of order, FO[<] - a result known as Kamp's theorem - [9] or equivalently to star-free languages.[10]
Computation tree logic (CTL) and linear temporal logic (LTL) are both a subset of CTL*, but are incomparable. For example,
Model checking and satisfiability against an LTL formula are PSPACE-complete problems. LTL synthesis and the problem of verification of games against an LTL winning condition is 2EXPTIME-complete.[11]
To check LTL specifications on infinite system runs, a common technique is to obtain a Büchi automaton that is equivalent to the model (accepts an ω-word precisely if it is the model) and another one that is equivalent to the negation of the property (accepts an ω-word precisely it satisfies the negated property) (cf. Linear temporal logic to Büchi automaton). In this case, if there is an overlap in the set of ω-words accepted by the two automata, it implies that the model accepts some behaviors which violate the desired property. If there is no overlap, there are no property-violating behaviors which are accepted by the model. Formally, the intersection of the two non-deterministic Büchi automata is empty if and only if the model satisfies the specified property.[12]
More generally, safety properties are those for which every counterexample has a finite prefix such that, however it is extended to an infinite path, it is still a counterexample. For liveness properties, on the other hand, every finite path can be extended to an infinite path that satisfies the formula.
Parametric linear temporal logic extends LTL with variables on the until-modality.[14]