Overview
Computation tree logic (CTL) expresses branching-time properties of transition systems. Its operators describe what happens on some or all computation paths, unlike LTL, whose formulas are evaluated along individual traces.
Syntax
CTL uses the path quantifiers A (“all paths”) and E (“some path”) together with temporal operators such as X (“next”) and U (“until”). Well-formed CTL formulas include EX\varphi, AX\varphi, and E[\varphi\,U\,\psi].
For example,
AG(\mathit{error}\to EF\,\mathit{recovered})
says that at every reachable state, if an error occurs, a recovery state is reachable along at least one continuation. It does not guarantee recovery along every continuation.
Semantics
CTL is interpreted over a Kripke structure whose transition relation is normally taken to be total, so every state has at least one successor and paths can be infinite. The meaning of EX\varphi is that some immediate successor satisfies \varphi; AX\varphi requires every immediate successor to do so.
Decidability and Complexity
CTL satisfiability is EXPTIME-complete. Model checking a finite Kripke structure against a CTL formula can be performed in time linear in the product of the structure size and formula length, under standard representations.
Relationships to Other Logics
CTL and LTL distinguish branching and linear perspectives, respectively. CTL* generalizes both in a common branching-time syntax, but its richer language has different complexity bounds.
References
- Edmund M. Clarke and E. Allen Emerson (1981). Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs.
- E. Allen Emerson (1990). Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Volume B.