Basic CTL (Computation Tree Logic) expresses properties on states in branching trees of computation.

CTL formulae are constructed from atomic propositions \(p\) and the following connectives: \[\varphi ::= \mathsf{true}~|~p~|~\varphi \land \varphi~|~\neg \varphi~|~AX\varphi~|~EX\varphi~|~A\,\varphi\ \mathcal{U}\ \varphi~|~E\,\varphi\ \mathcal{U}\ \varphi\]

The temporal quantifiers break down along two axes: \(A\) vs. \(E\):

\(A\)-quantifiers quantify over all paths forward from the current state

\(E\)-quantifiers quantify over some such path

\(X\) vs. \(\mathcal{U}\) for temporal specification

where \(X\) specifies the state immediately following the current state

\(\mathcal{U}\) asserts that some property holds at all points along a path until the first point at which some other property holds.

The derived operators \(AF\), \(EF\), \(AG\), and \(EG\) are also often used:

\[\begin{array}{l} AF\ \varphi \triangleq A\ \mathsf{true}\ \mathcal{U}\ \varphi \quad \quad EF\ \varphi \triangleq E\ \mathsf{true}\ \mathcal{U}\ \varphi \quad \quad\\ AG\ \varphi \triangleq \neg EF\ \neg\varphi\quad \quad EG\ \varphi \triangleq \neg AF\ \neg\varphi \end{array}\]

Intuitively,

\(AF\ \varphi\) (likewise \(EF\)) expresses the property that along all (some) paths, eventually (at some point now or in the future) \(\varphi\) will hold,

\(AG\ \varphi\) (likewise \(EG\)) expresses the property that along all (some) paths \(\varphi\) will always hold.

Our formulation of past-time CTL treats past-time operators is symmetric to future-time operators: \[\varphi ::= \ldots~|~A\,\varphi\ \mathcal{B}\ \varphi~|~E\,\varphi\ \mathcal{B}\ \varphi\]

Formally, the satisfaction of a CTL formula is defined with respect to a labeled transition system \(\mathcal{C}\) and a state \(q\) in that transition system. We write \(\mathsf{Paths}(\mathcal{C}, q)\) to denote the set of (non-branching) paths forward from \(q\) in \(\mathcal{G}\), where a path from \(q\) is simply a sequence of states \(q_0\ q_1\ ...\) such that \(q_0 = q\) and for all \(i\), there is some label \(\ell\) such that \((q_i, \ell, q_{i+1})\) is a valid transition in \(\mathcal{C}\). (We write \(\lambda_i\) to indicate the \(i\)th element of a path \(\lambda\).) Then the CTL satisfaction relation \(\mathcal{C}, q \models \varphi\) is defined as follows:

• \(\mathcal{C}, q \models \mathsf{true}\)

• \(\mathcal{C}, q \models p\) if \(p\) holds at \(q\)

• \(\mathcal{C}, q \models \varphi \land \psi\) if \(\mathcal{C}, q \models \varphi\) and \(\mathcal{C}, q \models \psi\)

• \(\mathcal{C}, q \models \neg\varphi\) if it is not the case that \(\mathcal{C}, q \models \varphi\)

• \(\mathcal{C}, q \models AX\varphi\) if \(\forall \lambda \in \mathsf{Paths}(\mathcal{C}, q).\ \mathcal{C}, \lambda_1 \models \varphi\)

• \(\mathcal{C}, q \models EX\varphi\) if \(\exists \lambda \in \mathsf{Paths}(\mathcal{C}, q).\ \mathcal{C}, \lambda_1 \models \varphi\)

• \(\mathcal{C}, q \models A\,\varphi\ \mathcal{U}\ \psi\) if \(\forall \lambda \in \mathsf{Paths}(\mathcal{C}, q).\ \exists i.\ \mathcal{C}, \lambda_i \models \psi\) and \(\forall j<i.\ \mathcal{C}, \lambda_j \models \varphi\)

• \(\mathcal{C}, q \models E\,\varphi\ \mathcal{U}\ \psi\) if \(\exists \lambda \in \mathsf{Paths}(\mathcal{C}, q).\ \exists i.\ \mathcal{C}, \lambda_i \models \psi\) and \(\forall j<i.\ \mathcal{C}, \lambda_j \models \varphi\)