Linear Temporal Logic - Syntax

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 a LTL formula;
• if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ, X ψ and φ U ψ are LTL formulas.

X is read as next and U is read as until. Sometimes, N is also used in place of X. 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 (globally)
• F for eventually (in the future)
• R for release
• W for weakly until