# Computation tree logic (CTL)

Based on [C. Baier, J.-P. Katoen: Principles of model checking, Ch. 6](https://mitpress.mit.edu/9780262026499/principles-of-model-checking/)

## Motivation for a branching time logic

In [Linear temporal logic (LTL)](/4Mhc2FywRF2mYqDprcJMAA), we can state properties over **all** possible computations starting at a given state. But what about properties that hold just for **some** computations? For some such statements one can leverage duality via negation $\lnot$, but this is not always possible.

Take for example: "For every computation it is always possible to return to the initial state".

Naively, one could try to require $\square \lozenge \mathrm{start}$ for every computation, i.e. $s \models \square \lozenge \mathrm{start}$, where the proposition $\mathrm{start}$ uniquely holds at the starting state. However, this is too strong: it requires a computation to **always** return to the starting state, not just **possibly**.

Indeed, one can show that it is **not possible** to express this intuitive property in LTL.

This and other examples motivate the definition of computation tree logic (CTL). LTL deals with linear time and path-based behavior starting from a state (via the trace of a state $s$), whereas CTL deals with **branching time** and **state-based** behavior, by investigating the computation tree of a given state $s$.

CTL also has the next operator $\bigcirc$ and the until operator $\mathbf{U}$. It adds in a universal quantifier $\forall$ and an existential quantifier $\exists$.

:::warning
**Beware.**
Even though it may seem so at first, it is not the case that CTL extends LTL in terms of expressivity. In fact, one can show that there are formulas in either language that are not expressible in the other one.
:::

## Syntax of CTL

Let $A$ be the set of atomic propositions. CTL **state formulas** are formed as follows:

$$ \Phi ::= \top \; | \; p \; | \; \Phi_1 \land \Phi_2 \; | \; \lnot \Phi \; | \; \exists \varphi \; | \; \forall \varphi$$

with $p \in A$ and $\varphi$ a CTL **path formula**. CTL path formulas are formed according to:

$$ \varphi ::= \bigcirc \Phi \; | \; \Phi_1 \mathbf{U} \Phi_2$$
with state formulas $\Phi, \Phi_1, \Phi_2$.

The path formulas $\bigcirc \Phi$ and $\Phi_1 \mathbf{U} \Phi_2$ have the same meaning as in LTL. They can be turned into state formulas by prefixing them with a quantifier:

* $\forall \varphi$ means that, in a state $\varphi$ holds if it holds **for all paths** starting in that state
* $\exists \varphi$ means that, in a state $\varphi$ holds if it holds **for some path** starting in that state

Similarly to LTL, we can derive the following operators:

1. **Eventually:**
a. $\exists \lozenge \Phi = \exists (\top \mathbf{U} \Phi)$ ("$\Phi$ holds **potentially**")
b. $\forall \lozenge \Phi := \exists (\top \mathbf{U} \Phi)$
("$\Phi$ is **inevitable**")

2. **Always:**
a. $\exists \square\Phi = \lnot \forall \lozenge \lnot \Phi$ ("$\Phi$ holds **potentially always**")
b. $\forall \square\Phi:= \lnot \exists \lozenge \lnot \Phi$
("$\Phi$ holds **invariantly**")

3. **Next:**
* For $\forall \bigcirc \Phi$ we say "For all paths next $\Phi$".

:::warning
**Beware.** Note that "always $\Phi$" cannot be obtained from duality in the sense that "$\square \Phi = \lnot \lozenge \lnot \Phi$". (Can you see why?)
:::

## Semantics of CTL

### CTL semantics for states and paths

Intuitively, the semantics can be illustrated as always:

Formally, we define the satisfaction relation for states and paths, respectively, as follows:

Let $p \in A$ be an atomic proposition, $ \mathcal T = (S, \Sigma, \to, I, A, \lambda)$ be a transition system without terminal states. Let $s \in S$ be a state, $\Phi, \Psi$ CTL state formulas, and $\varphi$ be a CTL formula.

The satisfaction relation for states $s$ is inductively generated by the following conditions:

* $s \models p$ iff $p \in \lambda(s)$
* $s \models \lnot \Phi$ iff $s \not \models \Phi$
* $s \models \Phi \land \Psi$ iff $s \models \Phi$ and $s \models \Psi$
* $s \models \exists \Phi$ iff $\rho \models \varphi$ for some $\rho \in \mathrm{Paths}(s)$
* $s \models \forall \Phi$ iff $\rho \models \varphi$ for all $\rho \in \mathrm{Paths}(s)$

The satisfaction relation for path formulas is defined as follows, given a path $\rho$:

* $\rho \models \bigcirc \Phi$ iff $\rho[1] \models \Phi$
* $\rho \models \Phi \mathbf{U} \Psi$ iff there exists $j \geq 0$ such that: $\pi[j] \models \Psi$ and for all $0 \leq k < j$: $\pi[k] \models \Phi$,
where for path $\rho = s_0 s_1 s_2 \ldots$ and integer $i \geq 0$, $\rho[i]$ denotes the $(i+1)$-th state of $\rho$, i.e. $\rho[i] = s_i$.

### CTL semantics for transition systems

Let $\Phi$ be a CTL state formula. Given a transition system $\mathcal T$ as before (in particular, without terminal states) the **satisfaction set** $\mathrm{Sat}_{\mathcal T}(\Phi)$, or $\mathrm{Sat}(\Phi)$ for short, for:

$$\mathrm{Sat}(\Phi) := \{ s \in S \; | \; s \models \Phi\}$$

The transition system $\mathcal T$ satisfies a CTL formula $\Phi$ if and only if $\Phi$ holds in all initial states of $\mathcal T$:

$\mathcal T \models \Phi$ iff for all $s_0 \in I$: $s_0 \models \Phi$.

Another way to say this is to require $I \subseteq \mathrm{Sat}(\Phi)$.

:::warning
**Exercise 1 (Semantics of CTL modalities).**
Let $\rho = s_0 s_1 s_2 \ldots$. Prove the following:
1. $\rho \models \lozenge \Phi$ iff there exists some $j \geq 0$ such that $s_j \models \Phi$
2. $s \models \exists \square \Phi$ iff there is a path $\rho \in \mathrm{Path}(s)$ such that $\rho[j] \models \Phi$ for all $j \geq 0$
3. $s \models \forall \square \Phi$ iff for all paths $\rho \in \mathrm{Path}(s)$ such that $\rho[j] \models \Phi$ for all $j \geq 0$
:::

:::warning
**Exercise 2 (CTL properties of transition systems).**
Consider the following transition system $\mathcal T = (S, \Sigma, \to, I, A, \lambda)$, with $I = \{s_0\}$:
For each of the following properties, decide for which states they hold. Does $\mathcal T$ satisfy them? Give arguments or counterarguments:
1. $\exists \bigcirc a$
2. $\forall \square a$
3. $\exists \lozenge (\exists \square a)$
:::

## Laws for CTL:

1. Duality laws:
$\forall \bigcirc \Phi \equiv \lnot \exists \bigcirc \lnot \Phi$
$\exists \bigcirc \Phi \equiv \lnot \forall \bigcirc \lnot \Phi$
$\forall \lozenge \Phi \equiv \lnot \exists \square \lnot \Phi$
$\exists \lozenge \Phi \equiv \lnot \forall \square \lnot \Phi$

2. Expansion laws:
$\forall \lozenge \Phi \equiv \Phi \lor \forall \bigcirc \forall \lozenge \Phi$
$\forall \square \Phi \equiv \Phi \land \forall \bigcirc \forall \square \Phi$
$\exists \lozenge \Phi \equiv \Phi \lor \exists \bigcirc \exists \lozenge \Phi$
$\exists \square \Phi \equiv \Phi \land \exists \bigcirc \exists \square \Phi$

3. Distributive laws:
$\forall \square (\Phi \land \Psi) \equiv \forall \square \Phi \land \forall \square \Psi$
$\exists \lozenge(\Phi \lor \Psi) \equiv \exists \lozenge \Phi \lor \exists \lozenge \Psi$