Temporal Logic

Origin. Arthur Prior developed tense logic (1957, 1967), applying modal logic to time. Amir Pnueli (1977) introduced Linear Temporal Logic (LTL) for program verification, winning the Turing Award for this work. Edmund Clarke and Allen Emerson developed Computation Tree Logic (CTL) and model checking; Joseph Sifakis, with Jean-Pierre Queille, developed model checking independently.

Models. Time and temporal relationships. How truth varies across moments. Two main paradigms: linear time (one future) vs branching time (multiple possible futures). Core questions: Will φ eventually hold? Has φ always held? Will φ hold until ψ holds?

Formalism.

Linear Temporal Logic (LTL): Syntax extends propositional logic with temporal operators: Xφ (next), Fφ (eventually/future), Gφ (always/globally), φUψ (until), φRψ (release).

Semantics: Models are infinite sequences of states σ = s₀, s₁, s₂, ... Truth at position i:

σ, i ⊨ Xφ iff σ, i+1 ⊨ φ
σ, i ⊨ Fφ iff ∃j ≥ i: σ, j ⊨ φ
σ, i ⊨ Gφ iff ∀j ≥ i: σ, j ⊨ φ
σ, i ⊨ φUψ iff ∃j ≥ i: σ, j ⊨ ψ and ∀k, i ≤ k < j: σ, k ⊨ φ

Computation Tree Logic (CTL): Branching time with path quantifiers. A (all paths) and E (some path) combined with temporal operators:

AGφ: on all paths, always φ
EFφ: on some path, eventually φ
AXφ: on all paths, next φ
A(φUψ): on all paths, φ until ψ

CTL*: Subsumes both LTL and CTL, allowing arbitrary combinations of path quantifiers and temporal operators.

Symbols.

Symbol	Unicode	Name	Meaning
X	—	Next	At the next moment
F	—	Future/Finally	At some future moment
G	—	Globally/Always	At all future moments
U	—	Until	φ holds until ψ holds
R	—	Release	Dual of until
W	—	Weak until	Until, but ψ may never come
A	—	All paths	On every possible future
E	—	Exists path	On some possible future
○	U+25CB	Next (alt)	Alternative symbol for X
◇	U+25C7	Eventually (alt)	Alternative symbol for F
□	U+25A1	Always (alt)	Alternative symbol for G
⊢	U+22A2	Derives	Syntactic derivation
⊨	U+22A8	Satisfaction	Truth at a position, state, or path
σ	U+03C3	Sigma	An infinite sequence of states

Metatheory. Kamp's theorem (1968) fixes the expressive ceiling of the linear family: over Dedekind-complete linear orders, the language with Until and Since is expressively complete for first-order logic in one free variable over <, and the LTL-definable ω-languages are exactly the star-free ones. The complexity of each member is settled. LTL satisfiability and model checking are PSPACE-complete (Sistla and Clarke 1985), with model checking in time O(|M| · 2^|φ|) and NLOGSPACE in the model for a fixed formula. CTL model checking runs in time O(|M| · |φ|) and is P-complete, which is why the early model checkers were built on CTL, while CTL satisfiability is EXPTIME-complete. CTL* model checking is PSPACE-complete and its satisfiability 2EXPTIME-complete. CTL and LTL are incomparable in both directions: EF p is CTL and not LTL, FG p is LTL and not CTL. All three embed in the modal μ-calculus, whose decidability rests on Rabin's tree theorem.

Applies to. Hardware and software verification. Model checking. Reactive system specification. Protocol verification. Planning in AI. Expressing liveness ("something good eventually happens") and safety ("nothing bad ever happens") properties.

Limitations. The propositional family defines only ω-regular sets, and LTL only the star-free ones, so "p holds at every even step" is beyond LTL and quantitative timing is beyond all of them: metric extensions are needed, and MTL with punctual constraints over dense time is undecidable (Alur and Henzinger). The linear/branching choice is a genuine fork rather than a matter of taste, since neither logic extends the other; a specification language must commit, and the two admit different verification algorithms and different notions of counterexample. Neither can relate two runs, so noninterference and other hyperproperties require quantification over traces. Lifting to first order is worse than costly: first-order temporal logic over ℕ is not recursively enumerable, and decidability is recovered only in the monodic fragment (Hodkinson, Wolter, Zakharyaschev 2000). Model checking is linear in the model and the model is exponential in the number of components.