# Linear temporal logic

In logic, linear temporal logic or linear-time temporal logic 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. Subsequently, LTL is sometimes called propositional temporal logic, abbreviated PTL.
Linear temporal logic is a fragment of first-order logic.
LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.

## Syntax

LTL is built up from a finite set of propositional variables AP, the logical operators ¬ and ∨, and the temporal modal operators X and U.
Formally, the set of LTL formulas over AP is inductively defined as follows:
• if p ∈ AP then p is an LTL formula;
• if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ, X ψ, and φ U ψ are LTL formulas.
Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators to write LTL formulas succinctly.
The additional logical operators are ∧, →, ↔, true, and false.
Following are the additional temporal operators.
• G for always
• F for eventually
• R for release
• W for weak until
• M for strong release

## Semantics

An LTL formula can be satisfied by an infinite sequence of truth evaluations of variables in AP.
These sequences can be viewed as a word on a path of a Kripke structure.
Let w = a0,a1,a2,... be such an ω-word. Let w = 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:
• w p if p ∈ w
• w ¬ψ if w ψ
• w φ ∨ ψ if w φ or w ψ
• w X ψ if w1 ψ
• w φ U ψ if there exists i ≥ 0 such that wi ψ and for all 0 ≤ k < i, wk φ
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, w ψ.
The additional logical operators are defined as follows:
• φ ∧ ψ ≡ ¬
• φ → ψ ≡ ¬φ ∨ ψ
• φ ↔ ψ ≡ ∧
• true ≡ p ∨ ¬p, where p ∈ AP
• false ≡ ¬true
The additional temporal operators R, F, and G are defined as follows:
• ψ R φ ≡ ¬
• F ψ ≡ true U ψ
• G ψ ≡ false R ψ ≡ ¬F ¬ψ

### Weak until and strong release

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. It is sometimes useful since both U and R can be defined in terms of the weak until:
• ψ W φ ≡ ∨ G ψψ Uφ R
• ψ U φFφ
• ψ R φφ W
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.
• ψ M φ ≡ ¬ ≡ ∧ F ψψ Rφ U
The semantics for the temporal operators are pictorially presented as follows.

## Equivalences

Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences which extend standard equivalences among the usual logical operators.

## Negation normal form

All the formulas of LTL can be transformed into negation normal form, where
• all negations appear only in front of the atomic propositions,
• only other logical operators true, false, ∧, and ∨ can appear, and
• only the temporal operators X, U, and R can appear.
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 size of the formula. This normal form is useful in translation from LTL to Büchi automaton.

## Relations with other logics

LTL can be shown to be equivalent to the monadic first-order logic of order, FO—a result known as Kamp's theorem— or equivalently star-free languages.
Computation tree logic and linear temporal logic are both a subset of CTL*, but are incomparable. For example,
• No formula in CTL can define the language that is defined by the LTL formula F.
• No formula in LTL can define the language that is defined by the CTL formulas AG or AG.
However, a subset of CTL* exists that is a proper superset of both CTL and LTL.

## Computational problems

Model checking and satisfiability problem against an LTL formula is PSPACE-complete. LTL synthesis and the problem of verification of games against an LTL winning conditions is 2EXPTIME-complete.

## Applications

;Automata-theoretic linear temporal logic model checking
;Expressing important properties in formal verification
;Specification language

## Extensions

Parametric linear temporal logic extends LTL with variables on the until-modality.