CTL* (Full Computation Tree Logic)

Origin. Emerson and Halpern (1986), "Sometimes and Not Never Revisited." The logic that subsumes both CTL and LTL by freely combining path quantifiers with linear temporal operators, resolving the expressiveness dispute between branching- and linear-time schools.

Models. Branching time with unrestricted mixing of path quantification and temporal modality. Interpreted over Kripke structures (computation trees). CTL fixes each temporal operator to a quantifier; LTL quantifies implicitly over all paths; CTL* lifts both restrictions, allowing arbitrary nesting.

Formalism.

Two syntactic categories: State formulas (hold at a state): φ ::= p | ¬φ | φ ∧ φ | A ψ | E ψ Path formulas (hold on a path): ψ ::= φ | ¬ψ | ψ ∧ ψ | X ψ | ψ U ψ | F ψ | G ψ

A and E quantify over paths from the current state; temporal operators apply to path formulas.

Semantics (structure M): State formula at s: M,s ⊨ A ψ iff every path π from s has M,π ⊨ ψ; E ψ iff some path does. Path formula on π: standard LTL clauses (X next, U until, F eventually, G always); a state formula on π is evaluated at π's first state.

Fragments recovered: CTL = CTL* where every temporal operator is immediately preceded by a path quantifier (AX, EU, AG, …). LTL = CTL* path formulas of the form A ψ with ψ quantifier-free. Strictly more expressive than either: e.g., E(GF p) (a path with p infinitely often) is CTL* but not CTL; A(FG p) is expressible where CTL cannot state it.

Duals: A ψ ≡ ¬E ¬ψ; F ψ ≡ true U ψ; G ψ ≡ ¬F ¬ψ; R (release) dual to U.

Symbols.

Symbol	Unicode	Name	Meaning
A	—	All paths	universal path quantifier
E	—	Exists path	existential path quantifier
X	—	Next	next state on path
F	—	Finally	eventually on path
G	—	Globally	always on path
U	—	Until	until on path
R	—	Release	dual of until

Metatheory. Model checking CTL* is PSPACE-complete (as hard as LTL; the branching structure adds no cost over the linear part). Satisfiability is 2EXPTIME-complete. CTL and LTL are expressively incomparable, and CTL* is the least logic containing both. Decision procedures go via automata on infinite trees (Rabin/parity tree automata); a sound and complete axiomatization exists (Reynolds, 2001).

Applies to. Reactive-system specification needing both branching and fairness/liveness. Hardware and protocol verification. As the semantic reference point unifying CTL tools (branching) and LTL tools (linear). Reasoning about mixed existential/universal path properties.

Limitations. Satisfiability and synthesis are 2EXPTIME — markedly costlier than CTL. The full logic is less used in practice than its CTL or LTL fragments precisely because of this cost. The two-level syntax is harder for practitioners to read than either fragment. Symbolic (BDD/SAT) methods are less directly applicable than for CTL.