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 */

Gerd Doeben-Henisch 2010-03-03