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, Allen Emerson, and Joseph Sifakis developed Computation Tree Logic (CTL) and model checking.

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

Metatheory. LTL satisfiability is PSPACE-complete. LTL model checking is NLOGSPACE in model size, PSPACE in formula size. CTL model checking is polynomial in both model and formula size (the reason CTL was preferred for early model checkers). CTL and LTL have incomparable expressiveness: some properties expressible in one but not the other. CTL* subsumes both but has higher complexity.

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. Discrete time only — continuous time requires different formalisms. The choice between LTL and CTL affects what properties are expressible: "on all paths eventually" (AF) vs "eventually on all paths" are different and only CTL distinguishes them. State explosion: model checking complexity is linear in model size, but models grow exponentially in system components. Past-time operators (since, historically) add expressiveness but are often omitted.