Computation Tree Logic

Theory of Computation


Syntax of CTL

State formula

A state formula in CTL is defined by the following grammar

$$\Phi:=true \ | \ a \ | \ \Phi_1\land\Phi_2 \ | \ \lnot \Phi \ | \ A\varphi \ | \ E\varphi$$

where a is an atomic proposition, and $\Phi_1,\Phi_2$ are state formula and $\varphi$ is a path formula defined by

$$\varphi=X\Phi \ | \ G\Phi \ | \ F\Phi \ | \ \Phi_1 U \Phi_2 \ | \ \Phi_1 W \Phi 2$$

Here the symbols stand for

  • A - for all

  • E - There exists

  • X - Next

  • G - Globally (always)

  • F - Finally (eventually)

  • U - Until

  • W - Weak until

Informally, the quantifiers should come in pairs, a quantifier over paths followed by a path specific one

Formal semantics

Given a set of atomic propositions AP and a transition system

$$TS=(S,\rightarrow,I,AP,L)$$
Satisfaction Relation

Defined recursively by

$$\begin{array}{ll} s \models t r u e & \\ s \models a & \text { iff } a \in L(s) \\ s \models \Phi_{1} \wedge \Phi_{2} & \text { iff } s\models\Phi_{1} \text { and } s \models \Phi_{2} \\ s \models \neg \Phi & \text { iff } s \not\models \Phi \\ s \models \mathbf{A} \varphi & \text { iff } \pi\models\varphi \text { for all } \pi \in \operatorname{Paths}(s) \\ s\models E\varphi & \text{ iff } \pi \models \varphi \text { for some } \pi \in \operatorname{Paths}(s) \end{array}$$

For a state $s\in S$ and by

$$\begin{array}{ll} \pi \models X \Phi & \pi_1\models\Phi\\ \pi\models \Phi_1U\Phi_2 & \text{ iff there is } i\geqslant 0 s.t. \pi_i\models\Phi_2 \text{ and } \pi_j \models \Phi_1 \text{ for all } 0\leqslant j <i \end{array}$$

Where the path \\$\pi\\\\$ is viewed as a sequence of states \\$\pi_0,\pi_1…$

CTL vs LTL

We can transform a state CTL formula into an LTL one by simply omitting the quantifiers over paths. The resulting formula is equivalent to the original one iff the property defined by the original, CTL, formula is expressible in the LTL.

CTL*

State formula in CTL*

A state formula in CTL* is defined by the following grammar

$$\Phi:=true \ | \ a \ | \ \Phi_1\land\Phi_2 \ | \ \lnot \Phi \ | \ A\varphi \ | \ E\varphi$$

where a is an atomic proposition, and $\Phi_1,\Phi_2$ are the state formulae and $\varphi$ is a path formula, defined by

$$\varphi=\Phi \ | \ \varphi_1\land\varphi_2 \ | \ \lnot \varphi \ | \ X\Phi \ | \ G\Phi \ | \ F\Phi \ | \ \Phi_1 U \Phi_2 \ | \ \Phi_1 W \Phi 2$$

where a path satisfies a state formula iff the state state of the path satisfies it:

$$\pi\models \Phi \text{ iff } \pi_0\models\Phi$$

Model Checking LTL

Lemma

A formula in CTL may be generated by the following grammar

$$\Phi:=\text {true}|a| \Phi_{1} \wedge \Phi_{2}|\neg \Phi| \mathbf{E X \Phi}\left|\mathbf{E}\left(\Phi_{1} \mathbf{U} \Phi_{2}\right)\right| \mathbf{E G} \Phi$$
Sat

Given a TS $(S,\rightarrow,I,AP,L)$, for a CTL-formula $\Phi$, denote by $Sat(\Phi)$ the subsets of states that satisfy $\Phi$, i.e. $Sat(\Phi)=\{s\in S|s\models \Phi\}$

Theorem

$Sat(\Phi)$ satisfies the following

  • Sat(true)=S
  • Sat(a) = $\{s\in S| a\in L(s)\}$ for every $a\in AP$
  • $Sat(\Phi_1\land\Phi_2)=Sat(\Phi_1)\cap Sat(\Phi_2)$
  • $Sat(\lnot\Phi)=S\backslash Sat(\Phi)$
  • $Sat(EX\Phi)=\{s\in S| succ(s) \cap Sat(\Phi) \neq \varnothing\}$
  • $Sat(E(\Phi_1U\Phi_2))$ is the smallest $T\subseteq S$ such that
    • $Sat(\Phi_2)\subseteq T$, and
    • $s\in Sat(\Phi_2)$ and $succ(s)\cap T\neq\varnothing\Rightarrow s\in T$
  • $Sat(EG\Phi)$ is the biggest $T\subseteq S$ such that
    • $T\subseteq Sat(\Phi)$, and
    • $s\in T \Rightarrow succ(s)\cap T \neq \varnothing$

where succ(s) is the direct successor of s, i.e. $succ(s)=\{t\in S|s\rightarrow t\}$