Ctl

CTL, or Computation Tree Logic, is a branching-time temporal logic used to specify properties of computation trees in model checking and formal verification. It is interpreted over Kripke structures or finite-state transition systems, where states satisfy atomic propositions and transitions reflect possible evolutions of a system. CTL distinguishes between path quantifiers and temporal operators, and every CTL formula has the form Q1 X1 Q2 X2 ... where Q are quantifiers A (for all paths) or E (exists a path) and Xi are temporal operators X (neXt), F (Finally), G (Globally), or U (Until). In CTL, the path quantifier immediately precedes a temporal operator, so the basic building blocks are EX p, AX p, EF p, AF p, EG p, AG p, and E[p U q], A[p U q].

Semantics: A state satisfies AX p if all immediate successor states satisfy p in the next state; EX p if there exists a successor state that satisfies p. AF p means along all paths, p eventually holds; EF p means there exists a path where p eventually holds. Similarly, AG p requires p to hold in all states along all paths globally, and EG p requires p to hold on some path globally. The Until operator combines state and path quantification as A[p U q] and E[p U q].

CTL is less expressive than CTL*, but allows model checking in time linear in the size of the model and the formula. It is widely used in hardware and software verification to assert properties such as safety (AG ¬error) and liveness (EF request).

Related concepts include LTL, which is linear-time temporal logic, and CTL*, which subsumes both LTL and CTL.