What does Computational Tree Logic (CTL) do?

1. Introduction

To define the model’s properties, we used LTL in the previous blog. Yet, can we express something like: “There is a possibility that \(p\) stays always true”? The short answer is NO.

The long answer is, however, this blog itself, where we look at another logic used in Model Checking: Computational Tree Logic (CTL).

2. Why is LTL not enough?

We take the following Kripke structure and the property we want to define: “There is a possibility that \(p\) stays always true”.

Clearly, the given Kripke structure satisfies that property for the path \(s_0, s_1, s_1, s_1, \dots\)

However, using only LTL, we cannot define this property correctly because LTL works on all possible paths and not on some of them. Here, \(G\,p\) is an incorrect suggestion, since\(p\) is not always satisfied on all paths (not in \(s_0, s_2, s_2, s_2, \dots\)).

What we want to express is rather something like:

\(\exists\) Path \(P\) such that: \(P \models G\,p\)

which we generally write as:

\(P \models EG\,p\)

This is exactly the syntax of Computational Tree Logic (CTL).

3. Computational Tree Logic (CTL)

3.1 Definition of syntax

Similar to LTL formulas, we define CTL over a set of atomic propositions \(AP\) as one of the following expressions:

True and False (like LTL)
\(p \in AP\): a propositional variable
\(\varphi \lor \psi\) where \(\varphi\) and \(\psi\) are CTL formulas
\(\lnot \varphi\) where \(\varphi\) is a CTL formula
\(EX\,\varphi\) (exists next)
\(\varphi\ EU\ \psi\) (exists until)
\(EG\,\varphi\) (exists globally)

3.2 Definition of semantics

3.2.1 Computational Trees

While LTL is evaluated over a single path of a Kripke structure, CTL is evaluated over a tree containing all possible paths starting at a state.

For instance, take the following Kripke structure:

Then the computational tree of \( s_0 \) is defined as follows (The tree is infinite)

3.2.2 Semantics

A CTL formula is evaluated to true/false over the computational tree of a Kripke structure. For a Kripke structure \(M\) and state \(s_0\), we write \((M, s_0) \models \psi\) when the computational tree starting at \(s_0\) satisfies \(\psi\).

\(M, s_0 \models True\) always holds.
\(M, s_0 \models False\) never holds.
\(M, s_0 \models p\) exactly when \(p \in L(s_0)\)
\(M, s_0 \models \varphi \lor \psi\) if \(M, s_0 \models \varphi\) or \(M, s_0 \models \psi\)
\(M, s_0 \models \lnot \varphi\) if \(M, s_0 \not\models \varphi\)
\(M, s_0 \models EX\,\varphi\) if \(\exists s’\) with \((s_0, s’) \in R\) and \(M, s’ \models \varphi\), i.e. it holds exactly when at least one of the next states of \( s_0 \) satisfies \( \varphi \)
\(M, s_0 \models \varphi\ EU\ \psi\) if \(\exists k \ge 0\) and a path \(s_0, s_1, \dots\) such that:
\[
\forall i,\; 0 \le i < k:\ M, s_i \models \varphi
\quad\text{and}\quad
M, s_k \models \psi
\]In other words, there must be way for \( \psi\) to eventually hold, and for \( \varphi \) to hold at every state before the first time \( \psi\) holds. In particular, if \( \psi\) already holds at the s0, then \( \varphi \, EU \, \psi\) holds immediately.
\(M, s_0 \models EG\,\varphi\) if \(\exists\) a path \(s_0, s_1, \dots\) such that \(\forall i \ge 0,\ M, s_i \models \varphi\) That is exactly what we wanted to describe previously as „There is a possibility that \(\varphi\) stays always true “.

3.3 Syntactic sugar

Similar to LTL, we define further operators for CTL to help us deal directly with more complex situations while making it still readable. This includes mainly the operators EF, AF, AG and AU. Like the “E” prefix stans for “Exists”, A stands for “All”.

Notation	Meaning	Derived from
\(\varphi \land \psi\)	Both hold	\(\lnot(\lnot \varphi \lor \lnot \psi)\)
\(\varphi \rightarrow \psi\)	If \(\varphi\) then \(\psi\)	\(\lnot \varphi \lor \psi\)
\(EF\,\varphi\)	Eventually holds in some path	\(True\ EU\ \varphi\)
\(AF\,\varphi\)	Eventually holds in all paths	\(\lnot EG\,\lnot \varphi\)
\(AG\,\varphi\)	Always holds in all reachable states	\(\lnot EF\,\lnot \varphi\)
\(\varphi\ AU\ \psi\)	Until holds for all paths	\( ((\lnot \psi) \, EU \, \lnot (\varphi \lor \psi)) \land EG \, (\lnot \psi) \)

3.4. Examples

We take the same Kripke structure as the previous blog. Decide whether each of the following CTL formulae hold.

3.4.1. The Kripke structure:

3.4.2. The formulae:

\(F_1 = AF\,p\)
\(F_2 = EG\,p\)
\(F_3 = EX\,q\)
\(F_4 = EX\,EG\,q\)
\(F_5 = EX\,AF(\lnot p \land \lnot q)\)
\(F_6 = AF\,EG\,q\)
\(F_7 = EX\,\lnot p\)
\(F_8 = AG\,EF\,p\)
\(F_9 = EF\,AG\,q\)
\(F_{10} = AX\,AX\,(EG\,q \Rightarrow \lnot p)\)
\(F_{11} = (p \land q)\; E\,U\; (p \land \lnot q)\)
\(F_{12} = AX\bigl((AX\,p)\; A\,U\; (AX\,q)\bigr)\)

3.4.3. Solution and explanation

Formula	Truth value	Explanation
\(F_1\)	True	“In all paths, \(p\) will eventually hold,” which is true because \(p\) holds in the initial state.
\(F_2\)	True	“There is a path at which \(p\) will always hold” is true for the path \(s_0, s_1, s_0, s_1, s_0, s_1, \dots\).
\(F_3\)	False	“\(q\) holds in one of the next states” is false as all the next states do not contain \(q\) in their labels.
\(F_4\)	False	“There is one path starting at one of the next states at which \(q\) will always hold.” This is false because \(q\) does not hold at any of the next states.
\(F_5\)	True	“There is a next state at which all paths will reach a state where neither \(p\) nor \(q\) holds.” This is true because \(s_3\) is always reachable from any state.
\(F_6\)	True	“We reach in all possible paths a state from which at least a path will satisfy \(q\) forever.” The state we can reach is \(s_2\), from which we can stay at \(s_2\) forever, meaning that \(EG\,q\) holds at that state. As this state is always reachable, the expression is true.
\(F_7\)	True	“One of the next states does not satisfy \(p\)” is true for the next state being \(s_3\).
\(F_8\)	True	“In all possible paths it will always hold that we can reach a state where \(p\) holds.” This is true because all the states are able to reach \(s_1\) or \(s_0\).
\(F_9\)	False	“We can reach a state where \(q\) is always satisfied in all paths.” This is not true as \(q\) can never be satisfied in all possible paths: at \(s_0\), \(q\) will be false at its next state \(s_1\); at \(s_2\), \(q\) will be false at its next state \(s_3\).
\(F_{10}\)	True	“After any two steps: if we can satisfy \(q\) forever on some path, then \(p\) cannot be true.” The condition “we can satisfy \(q\) forever on some path” can only be true when we are at \(s_2\), as \(q\) is not satisfied in \(s_1\) and \(s_3\), and cannot be satisfied after one step if we begin at \(s_0\). This translates the statement to “After any two steps: if we are at \(s_2\), then \(p\) cannot be true,” which is true as \(p\) is false at \(s_2\).
\(F_{11}\)	True	“There is a path where both \(p\) and \(q\) are true until the first time where neither of them is satisfied.” This is the case for the path \(s_0, s_3, s_1, s_2, s_2, s_2, \dots\) as \(p\) and \(q\) are satisfied at \(s_0\), and neither is at the next state \(s_3\).
\(F_{12}\)	True	“In all next states, all paths satisfy the statement ‘all next states satisfy \(p\) until the first time all next states satisfy \(q\)’. ” Our next states are \(s_1\) and \(s_3\). All next states of \(s_1\) satisfy \(q\), meaning that \(AX\,q\) holds at \(s_1\), meaning also that \(\bigl((AX\,p)\ AU\ (AX\,q)\bigr)\) is already true at \(s_1\). The only next state of \(s_3\) is \(s_1\) at which \(p\) holds, meaning that \(AX\,p\) holds at \(s_3\). One step after, we land on \(s_1\) which satisfies \(AX\,q\), which means that \(\bigl((AX\,p)\ AU\ (AX\,q)\bigr)\) is also true at \(s_3\). All in all, \(\bigl((AX\,p)\ AU\ (AX\,q)\bigr)\) is true in all next states, and thus \(F_{12}\) is true.

4. Is CTL stronger than LTL?

There exist LTL formulas that cannot be expressed in CTL. The classic example is:

\[
GF\,p \not\equiv AF\,AG\,p
\]

Consider the Kripke structure with two infinite loops, one with \(p\) always true, one with \(p\) always false. Then:

\(GF\,p\) is true because there exists a path where \(p\) holds infinitely often,
but \(AF\,AG\,p\) is false, because not all paths eventually guarantee that \(p\) always holds.

5. Summary

In this blog, we explored the differences between LTL and CTL in the context of model checking. We saw that some properties, like “there exists a path where a proposition remains true forever,” cannot be expressed in LTL but are naturally captured in CTL using operators like \(EG\), \(AF\), and \(AG\).

We provided examples using a Kripke structure to evaluate multiple CTL formulas, explaining which formulas hold and why. The key takeaway is that CTL allows us to reason about all possible paths or existential paths in a Kripke structure, whereas LTL formulas are interpreted over single paths.

Understanding these distinctions is crucial for formally verifying system properties and choosing the appropriate logic for a given model checking task.