CTL Model Checking

Fixed-point Theory

Complete Lattice

Complete lattice is a partially-ordered set which has join ($\cup$) and meet ($\cap$) operators. The former generates the least lower bound and the latter the greatest upper bound. The state space of a Kripke model forms a complete lattice under containment, i.e. $(2^S, \subseteq)$ is a complete lattice.

Monotonic Function

$F$ is monotonic if $\forall a < b$, $F(a) < F(b)$.

Tarski's Theorem

A monotonic function over a complete lattice has the least and the greatest fixed point.

Kleene's Theorem

The mentioned fixed points can be calculated this way. Assume $F$ is a monotonic function and $\cup$-continuous (increments), the least fixed point must be reached (this chain converges): $$\emptyset \subseteq F(\emptyset) \subseteq F(F(\emptyset)) \subseteq \ldots$$

Instead, if $F$ is $\cap$-continuous (decrements), the greatest fixed point is obtained by, $$S \supseteq F(S) \supseteq F(F(S)) \supseteq \ldots$$

Formula Rewriting

All CTL formulae can be rewritten in terms of $\neg, \wedge, \mathbf{EX}, \mathbf{EU}, \mathbf{EG}$ only.

• $\mathbf{AG}\phi = \neg \mathbf{EF} \neg \phi$
• $\mathbf{EF}\phi = \mathbf{E}(\top \mathbf{U} \phi)$
• $\mathbf{A}(\phi_1 \mathbf{U} \phi_2 ) = \neg \mathbf{E}(\neg \phi_2 \mathbf{U} (\neg \phi_1 \wedge \neg \phi_2 )) \wedge \neg \mathbf{EG}\neg \phi_2$
• $\mathbf{AX} \phi = \neg \mathbf{EX} \neg \phi$

Although irrelevant at this context, but it is worthy to note that $\mathbf{EG}\phi = \mathbf{E}(\bot \mathbf{R} \phi)$, this is to say $\phi$ is never released (has to be true forever).

Tableaux Rules

• $\mathbf{EF}\phi = \phi \vee \mathbf{EXEF}\phi$
• $\mathbf{EG}\phi = \phi \wedge \mathbf{EXEG}\phi$
• $\mathbf{E}(\phi \mathbf{U} \psi) = \psi \vee (\phi \wedge \mathbf{EXE}(\phi \mathbf{U} \psi))$

Pre-Image

In CTL model checking, the calculating unit is a set of states that satisfy some formula $\phi$, noted as denotation $[\phi]$. Pre-Image maps the image (in the range) back to the domain (its pre-image). It is thus defined, $$\mathsf{PreImage}([\phi]) = \{s | \exists (s, s') \in R \wedge s' \in [\phi]\}$$

$\mathsf{PreImage}$ is a monotonic function over the complete lattice $(2^S, \subseteq)$, thus Kleene's theorem applies. Pre-Image matches the idea of $\mathbf{EX}$, i.e. $[\mathbf{EX}\phi]$ is the pre-image of $[\phi]$.

Fixed points for CTL Model Checking

According to tableaux rules, $\mathbf{EG}$, $\mathbf{EF}$, $\mathbf{EU}$s are written in the form of fixed points ($\nu$: greatest, $\mu$: least.).

• $[\mathbf{EG}\phi] = \nu Z. ([\phi] \cap [\mathbf{EX}Z])$
• $[\mathbf{EF}\phi] = \mu Z. ([\phi] \cup [\mathbf{EX}Z])$
• $[\mathbf{E}(\phi \mathbf{U} \psi)] = \mu Z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}Z]))$

So given a CTL formula $\phi$, after rewriting, we apply the set operations for negations (complement the set) and disjunctions (union), and fixed points for temporal formulas. We say $M \models \phi$ iff $I \subseteq [\phi]$.

Clarke-Emerson Theorem

The theorem gives CTL formula an iterative interpretation of their denotational semantics. \begin{align*} [\mathbf{EG} \phi] &= \nu z. ([\phi] \cap [\mathbf{EX} z]) \\ [\mathbf{E}(\phi \mathbf{U} \psi)] &= \mu z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}z])) \\ [\mathbf{EF} \phi] &= \mu z. ([\phi] \cup [\mathbf{EX} z] \end{align*}

Appendix

• $[\mathbf{EX} \phi]$ is the existential pre-image of $[\phi]$.
• $\nu z. F z$ calculates the greatest fixed point.
• $\mu z. F z$ calculates the least fixed point.
• $\mathbf{EF} \phi = \mathbf{E}(\top \mathbf{U} \phi)$

Expressiveness of LTL, CTL, CTL*

Consider the following examples.

• $\mathbf{GF}p = \mathbf{AGAF}p = \mathbf{AGF} p$
• The existential quantifier is not possible in LTL. E.g., $\mathbf{EF}p$
• $\mathbf{FG}p \neq \mathbf{AFAG}p$, see Fig 1.
• $\mathbf{EFG}p \neq \mathbf{FG}p \neq \mathbf{EFAG} p$
• $\phi \in$ LTL $\Rightarrow \mathbf{A} \phi \in $CTL*
• All CTL formulae are automatically CTL*.

Fig. 1 A Kripke Model $M \models \mathbf{FG}p$ but $M \not \models \mathbf{AFAG}p$

It says

• They can all express some common formulae.
• Some CTL formulae are not covered in LTL.
• Some LTL formulae can not be expressed by CTL.
• Some CTL* formulae are covered neither in CTL nor LTL.
• CTL* subsumes both CTL and LTL.