A propositional, branching-time temporal logic for which formulas can be checked in linear time. An acronym for Computation Tree Logic.

CTL differs from CTL* in that in CTL path quantifiers (E and A) always appear with temporal operators (F, G, X, U, etc.). Therefore CTL formulas are state formulas.