Temporal Logic: LTL and CTL

Core Idea

Temporal logics extend propositional logic with operators that express properties over time, enabling specification of system behaviors like "every request is eventually granted" (liveness) or "the system never enters an error state" (safety). Linear Temporal Logic (LTL) reasons about individual execution paths using operators like G (globally/always), F (finally/eventually), X (next), and U (until). Computation Tree Logic (CTL) reasons about the branching tree of all possible futures, combining path quantifiers (A = all paths, E = some path) with temporal operators. LTL and CTL have incomparable expressive power: each can express properties the other cannot.

Explainer

Temporal logic provides the specification language for model checking. While propositional logic can describe what is true at a single moment, temporal logic adds operators that talk about the evolution of truth over time — what was true, what will become true, what remains true forever. Two families dominate formal methods: Linear Temporal Logic (LTL) and Computation Tree Logic (CTL).

LTL views time as a single infinite sequence of states — one execution path. Its temporal operators modify propositions relative to positions along this path. G p (globally p) means p holds at every future position. F p (finally p) means p holds at some future position. X p (next p) means p holds at the immediately next position. p U q (p until q) means p holds continuously until q becomes true (and q must eventually become true). Complex properties compose these: G(request -> F grant) says "always, a request is followed by an eventual grant." LTL formulas are implicitly universally quantified over all execution paths — the property must hold on every possible run of the system.

CTL views time as a branching tree: at each state, the system may transition to multiple possible successor states (representing nondeterminism or concurrency). CTL combines path quantifiers (A = "for all paths from this state," E = "there exists a path from this state") with state-level temporal operators (G, F, X, U). These always appear in pairs: AG p, EF p, AX p, EU(p,q), etc. The formula AG(not deadlock) means "on all paths, globally, no deadlock occurs." The formula AG(EF restart) means "from every reachable state, on all paths, there exists a path reaching a restart state" — the system can always potentially recover.

The two logics are incomparable in expressiveness. LTL can express fairness properties like F(G p) ("eventually p holds forever") that CTL cannot. CTL can express branching properties like AG(EF p) ("p is always reachable") that LTL cannot. The unifying logic CTL* subsumes both, allowing arbitrary nesting of path quantifiers and temporal operators, but its model checking algorithms are more expensive. In practice, the choice between LTL and CTL depends on the property: use LTL for path-centric properties (fairness, response patterns) and CTL for branching properties (reachability, recoverability).

The distinction between safety and liveness properties cuts across both logics. Safety properties (G not bad) say "nothing bad ever happens" — they are violated by finite prefixes. Liveness properties (G(request -> F response)) say "something good eventually happens" — they can only be violated by infinite traces where the good thing never occurs. This distinction profoundly affects model checking algorithms: safety violations produce finite counterexample traces, while liveness violations produce "lasso" counterexamples (a finite stem followed by an infinitely repeating cycle). Understanding which temporal operators express safety vs. liveness is essential for writing effective specifications.