Computation Tree Logic

Origin. Clarke and Emerson introduced CTL (1981). Branching time: tree of possible futures. Path quantifiers + temporal operators. Foundation for symbolic model checking. CTL* combines CTL and LTL. Tools: SMV, NuSMV, UPPAAL.

Models. Branching futures in state space. System: Kripke structure with states and transitions. CTL: properties of computation tree rooted at state. Path quantifiers: A (all paths), E (some path). Temporal: X, F, G, U. Interleaved: AXφ, EFφ, AGφ, etc.

Formalism.

Syntax (CTL): State formulas: φ ::= p | ¬φ | φ ∧ ψ | AXφ | EXφ | A[φUψ] | E[φUψ] | AFφ | EFφ | AGφ | EGφ

Path quantifiers must immediately precede temporal operators.

Semantics (Kripke structure M, state s):

M, s ⊨ AXφ iff all successors satisfy φ
M, s ⊨ EXφ iff some successor satisfies φ
M, s ⊨ AFφ iff on all paths from s, eventually φ
M, s ⊨ EFφ iff on some path from s, eventually φ
M, s ⊨ AGφ iff on all paths from s, always φ
M, s ⊨ EGφ iff on some path from s, always φ
M, s ⊨ A[φUψ] iff on all paths, φ until ψ
M, s ⊨ E[φUψ] iff on some path, φ until ψ

CTL:* Full combination: path quantifiers + LTL path formulas. A(GFφ) — on all paths, infinitely often φ. More expressive than both CTL and LTL.

Minimal set: EX, EG, EU sufficient (others definable). AXφ = ¬EX¬φ, AFφ = ¬EG¬φ, etc.

Fairness: Fair CTL: restrict to fair paths. Strong fairness, weak fairness.

Symbols.

Symbol	Unicode	Name	Meaning
A	—	All paths	Universal path
E	—	Exists path	Existential path
X	—	Next	Next state
F	—	Finally	Eventually
G	—	Globally	Always
U	—	Until	Until
R	—	Release	Dual of until

Metatheory. CTL model checking is P-complete (linear in model × formula). Symbolic model checking: BDDs, SAT. CTL and LTL incomparable expressively. CTL* subsumes both. Satisfiability: EXPTIME-complete. Bisimulation: CTL preserved. Complete axiomatization exists.

Applies to. Hardware verification (Intel, IBM). Protocol verification. Cache coherence. Mutual exclusion. Deadlock detection. Liveness properties. Reactive synthesis.

Limitations. Branching not always intuitive. Some LTL properties not expressible (AFG). CTL* is expensive (2EXPTIME). Fairness requires extensions. Less compositional than LTL. State explosion in explicit model checking.