Computation tree logic

Definition

Let $AP$ be a set of atomic propositions. A Kripke structure is a triple $M = (S, R, L)$ of a set $S$ of states, a relation $R \subseteq S \times S$ and a labelling $L \colon S \to \mathcal{P}(AP)$. The relation $R$ is required to be total: each state has at least one successor. A path from $s$ is an infinite sequence $\pi = s_0 s_1 s_2 \cdots$ with $s_0 = s$ and $(s_i, s_{i+1}) \in R$ for all $i$. The formulas of computation tree logic are given by the grammar $$\varphi ::= p \mid \neg \varphi \mid \varphi \land \varphi \mid EX\varphi \mid EG\varphi \mid E[\varphi \, U \, \varphi], \qquad p \in AP.$$ The relation $M, s \models \varphi$ is defined by induction on $\varphi$:

1. $M, s \models p$ if and only if $p \in L(s)$, and $\neg$, $\land$ have their Boolean meaning;
2. $M, s \models EX\varphi$ if and only if $M, s' \models \varphi$ for some $s'$ with $(s, s') \in R$;
3. $M, s \models EG\varphi$ if and only if some path $s_0 s_1 \cdots$ from $s$ has $M, s_i \models \varphi$ for all $i \ge 0$;
4. $M, s \models E[\varphi \, U \, \psi]$ if and only if some path $s_0 s_1 \cdots$ from $s$ and some $j \ge 0$ have $M, s_j \models \psi$ and $M, s_i \models \varphi$ for all $0 \le i < j$.