Linear Temporal Logic

Origin. Pnueli introduced LTL for program verification (1977). Temporal operators over infinite sequences. Linear time: one future path. Foundation for model checking (Vardi, Wolper). Tools: SPIN, NuSMV, SPOT. Turing Award to Pnueli (1996).

Models. Properties of infinite traces. System execution: infinite sequence of states. LTL: properties that hold along any such sequence. Safety: nothing bad happens (G¬error). Liveness: something good happens (GF response). Fairness expressible.

Formalism.

Syntax: φ ::= p | ¬φ | φ ∧ ψ | Xφ | φUψ | Fφ | Gφ

Semantics (over infinite word w = w₀w₁w₂...):

w, i ⊨ p iff p ∈ wᵢ
w, i ⊨ Xφ iff w, i+1 ⊨ φ (next)
w, i ⊨ Fφ iff ∃j≥i. w, j ⊨ φ (finally/eventually)
w, i ⊨ Gφ iff ∀j≥i. w, j ⊨ φ (globally/always)
w, i ⊨ φUψ iff ∃j≥i. (w, j ⊨ ψ ∧ ∀k. i≤k<j → w, k ⊨ φ) (until)

Derived operators:

Fφ = ⊤Uφ
Gφ = ¬F¬φ
φRψ = ¬(¬φU¬ψ) (release)
φWψ = (φUψ) ∨ Gφ (weak until)

Common patterns:

Response: G(request → F response)
Precedence: (¬q)U p ∨ G¬q
Invariance: Gφ
Recurrence: GFφ
Persistence: FGφ

Automata connection: LTL formula → Büchi automaton. Model checking: product with system, check emptiness.

Symbols.

Symbol	Unicode	Name	Meaning
X	—	Next	Next state
F	—	Finally	Eventually
G	—	Globally	Always
U	—	Until	Strong until
R	—	Release	Dual of until
W	—	Weak until	Until or always
ω	U+03C9	Omega	Infinite sequence; the order type of the model
⊨	U+22A8	Satisfaction	Holds at position i of a word
⊤	U+22A4	Verum	Used in Fφ = ⊤Uφ

Metatheory. LTL is sound and complete over the class of ω-sequences; Gabbay, Pnueli, Shelah, and Stavi (1980) gave the axiomatization, and Gabbay (1981) the separation theorem. Satisfiability and validity are PSPACE-complete, settled by Sistla and Clarke (1985); model checking is PSPACE-complete as well, running in time O(|M| · 2^|φ|) and in NLOGSPACE in the size of the model for a fixed formula. Kamp's theorem (1968) is the expressiveness result: over Dedekind-complete linear orders the language with Until and Since is expressively complete for first-order logic with one free variable over <, and over ω the future fragment with Until alone already suffices. Equivalently, the LTL-definable ω-languages are exactly the star-free (aperiodic) ω-regular languages. Every satisfiable formula has an ultimately periodic model uvʷ with |u| + |v| exponential in |φ|, which is why the automaton A_φ can be taken with 2^O(|φ|) states (Vardi and Wolper 1986). Realizability and synthesis are 2EXPTIME-complete (Pnueli and Rosner 1989).

Applies to. Hardware verification. Software model checking (SPIN). Reactive systems. Protocol verification. Requirements specification. Runtime verification. Robotics (mission specification).

Limitations. LTL captures exactly the star-free ω-languages, so it cannot express "p holds at every even position" or "p occurs an even number of times" — ω-regular properties that are not aperiodic. Reaching the full ω-regular class requires quantified propositional temporal logic, extended temporal logic, or the μ-calculus, and QPTL's satisfiability is non-elementary (Sistla, Vardi, Wolper). Being interpreted over one trace at a time, LTL cannot quantify over paths: EF p is not expressible, and LTL and CTL are expressively incomparable in both directions. Hyperproperties such as noninterference relate two traces and are outside the logic entirely, requiring HyperLTL. There is no metric on time, so bounded-response constraints need MTL or TPTL. The exponential in the automaton construction is not an artifact — families of formulas are known whose smallest equivalent Büchi automaton is exponentially large.