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

Metatheory. LTL satisfiability is PSPACE-complete. Model checking is PSPACE in formula, NLOGSPACE in model. Expressively equivalent to first-order logic over (ω, <). Star-free regular ω-languages. Büchi automata: doubly exponential translation. Complete axiomatization exists.

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

Limitations. Linear time: no branching choices. Cannot express "there exists a path." Doubly-exponential automata translation. Some properties need CTL (reset, all paths). Past operators sometimes needed (PLTL). Finite traces require adaptation (LTLf).