Examples of CTL-Expressions with Interpretations

We assume as an example automaton the automaton $a1$ in figure 5.5.6 from above along with the execution graph related to $a1$ in figure 5.3.

Some examples of CTL-formula and their interpretation relativ to $a1$:

1. $a1 \models \textbf{E}\textbf{X}a$ /* In the execution graph of $a1$ there is a run $\varrho_{1}$ as a path $\pi_{1}$ where at position i= 0+1 = 1 is the state $q_{1}$ with property $a$ which follows state $q_{0}$ with property $A$ */
2. $a1 \models \textbf{E}\textbf{F}c$ /* In the execution graph of $a1$ there is a run $\varrho_{2}$ as a path $\pi_{2}$ where at position i= 2 is the state $q_{3}$ with property $c$ */
3. $a1 \models \textbf{E}\textbf{G}b$ /* In the execution graph of $a1$ there is a run $\varrho_{3}$ as a path $\pi_{3}$ where on all positions there is a state with property $b$; this is the path $\langle q_{0}, q_{4},...\rangle$ */
4. $a1 \models \textbf{E}(b\textbf{U}c)$ /* In the execution graph of $a1$ there is a run $\varrho_{2}$ as a path $\pi_{2}$ and in this run there is the state $q_{3}$ at position i=2 with property $c$ and at positions 1-2 are the states $q_{1},q_{2}$ with property $b$ */

5. $a1 \models \textbf{A}\textbf{X}e$ /* In the execution graph of $a1$ it holds for paths at positions i= 0+1 = 1 that there are states $\{q_{1}, q_{2},q_{4}\}$ with property $e$ which are following state $q_{0}$ */

6. $a1 \models \textbf{A}\textbf{F}e$ /* In the execution graph of $a1$ it holds for all paths at positions i= 0+1 = 1 that there are states $\{q_{1}, q_{2},q_{4}\}$ with property $e$ which are following state $q_{0}$ */

7. $a1 \models \textbf{A}\textbf{G}d$ /* In the execution graph of $a1$ it holds for all paths at all positions that there are states with property $d$ */

8. $a1 \models \textbf{A}(g\textbf{U}e)$ /* In the execution graph of $a1$ it holds for all paths that there are positions whose states hold property $e$ and these states are successors of states which have the property g */