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 checks a timed-CTL subset over timed automata.

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
⊨	U+22A8	Satisfaction	Holds at a state of a Kripke structure
¬	U+00AC	Negation	Used in the duals AXφ = ¬EX¬φ

Metatheory. CTL is sound and complete with respect to the class of Kripke structures with a total transition relation, where every state begins at least one infinite path; the axiomatization is due to Emerson and Halpern (1982, 1985). It has the finite model property in the strong form of a small model property: a satisfiable formula has a finite model of size exponential in the formula, which gives the EXPTIME upper bound, and satisfiability is EXPTIME-complete. Model checking is the reason CTL was adopted first: Clarke, Emerson, and Sistla (1986) gave an algorithm running in time O(|M| · |φ|), linear in both arguments, and the problem is P-complete (Schnoebelen). CTL is invariant under bisimulation, and Browne, Clarke, and Grumberg (1988) proved the converse on finite structures — CTL-equivalence and bisimilarity coincide there. CTL translates linearly into the alternation-free fragment of the modal μ-calculus. It is expressively incomparable with LTL and a proper fragment of CTL*.

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

Limitations. The requirement that every temporal operator be immediately preceded by a path quantifier is what makes model checking linear and what makes the logic weak: path formulas cannot be combined, so the LTL property FG p has no CTL equivalent, and fairness assumptions of the form GF p → GF q cannot be written at all. Fair CTL recovers them only by building the fairness constraint into the semantics of the quantifiers rather than into the syntax. Being bisimulation-invariant, CTL cannot express any property of an individual trace, and its counterexamples are trees rather than single runs. Satisfiability is EXPTIME-complete against LTL's PSPACE, and moving to CTL* to regain the missing path properties costs 2EXPTIME. Model checking is linear in the model, but the model is exponential in the number of concurrent components, so state explosion is the operative bound.