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.

Metatheory. Model checking CTL* is PSPACE-complete (Emerson and Lei): state subformulas are handled by recursion and path subformulas by the LTL procedure, so the branching structure costs nothing beyond the linear part. Satisfiability is 2EXPTIME-complete, with the lower bound due to Vardi and Stockmeyer (1985) and the upper bound due to Emerson and Jutla (1988); the decision procedure goes through automata on infinite trees, and a satisfiable formula has a finite model of doubly exponential size. Reynolds (2001) gave a sound and complete axiomatization for the class of all total transition structures, an open problem for fifteen years after the logic was defined. CTL and LTL are expressively incomparable — EF p is CTL and not LTL, FG p is LTL and not CTL — and CTL* is the least logic containing both. CTL* is bisimulation-invariant and is strictly weaker than the modal μ-calculus, into which it translates at alternation depth two. Over trees it has been shown equivalent in expressive power to monadic path logic (Hafer and Thomas; Moller and Rabinovich).

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. The path formulas of CTL* are exactly LTL formulas, so along any single path the logic defines only star-free properties: "some path on which p holds at every even step" is ω-regular and not expressible, and CTL* is therefore a proper fragment of the modal μ-calculus rather than a maximal branching-time logic. The 2EXPTIME bound on satisfiability and on synthesis is a lower bound as well as an upper one, so no reformulation of the decision procedure removes the tower. Model checking is PSPACE-complete, inheriting LTL's cost and losing CTL's linear-time algorithm, and the symbolic fixpoint methods that make CTL practical apply directly only to the CTL fragment — the path subformulas require an automaton construction instead. Being bisimulation-invariant, CTL* cannot relate two distinct paths, so information-flow and other hyperproperties remain outside it.

© 2026 Lingenic LLC