General Idea

Before we will go into the details and further improvements of model checking we will discuss first a simple example following the outline of Bérard et al. (2001)[34]:chapt.3.

Figure 8.1: Model Checking Scenario

We will apply the idea of a model checking algorithm presented by Bérard et al. (2001)[34]:chapt.3 to the example automaton $a1$ in figure 5.5.6 along with a transition graph $g1$ in figure 5.2 and the execution graph in figure 5.3.

To construct such an algorithm we will use as a guide the following list of CTL-expressions:

1. Propositions: $\phi$ as $p, \neg p, p \wedge q$
2. Temporal operators: $X\phi, (\phi U \psi)$
3. Path operators: $E\phi$

If one wants -by practical reasons- more operators one can introduce more operators based on proven equivalences (cf. 6.2 ).

The basic idea of the algorithm of Bérard et al. is to start checking the CTL-expression $\Phi$ assuming the most simple cases and then, if the expression $\phi$ is combined of subformulas $\psi_{1},\psi_{2},...$ to check these subformulas again as long as they are not atomic propositions.

We assume:

1. $Q = \{q_{0}, q_{1},q_{2},q_{3}, q_{4} \}$
2. $I = \{q_{0}\}$
3. $F = \{ q_{1},q_{3}\}$
4. $\Sigma = \{b,1,2,3,x,c,o,n,t \}$
5. $\Xi = \{t,1,2,3,e,n,d,x,c,o,n,t \}$
6. $\Delta = \{\langle q_{0},''b1'',''t1'' q_{1}\rangle, \langle q_{0},''b2'',''t2... ...''tendx'', q_{3}\rangle, \langle q_{4},''cont'',''tendcont'', q_{4}\rangle,\}$
7. $l = \{ (q_{0}, \{a,b,d,g \}), (q_{1}, \{a,d,e,f \}), (q_{2}, \{b,d,e \}), (q_{3}, \{c,d,f \}), (q_{4}, \{a,b,d,e,f \}) \}$
8. $AP = PROP = \{a,b,c,d,e,f,g \}$

The whole checking algorithm consist of a sequence of different subchecks starting with case 1 with follow up cases if case 1 is not sufficient. Lets call the whole algorithm docheck:

• Case 1: $\phi = P$. P is an atomic proposition. One has to check whether $P \in l(q)$ for each state $q \in Q$. If q.phi $\in l(q)$ then q.phi := true, otherwise q.phi := false.
• Example: $\phi = a$ and $a \in l(q_{0}) \cup l(q_{1}) \cup l(q_{4})$, therefore q.phi = true.

• Case 2: $\phi = \neg \psi$. Call algorithm $docheck(\psi)$. One has to check for all $q \in Q$ whether q.phi := not(q.psi).
• Example: $\phi = \neg a$. Because $docheck(a)$gives q.psi = true for $l(q_{0}) \cup l(q_{1}) \cup l(q_{4})$ we get for these states q.phi := not(true) = false. But $a \not\in l(q_{2}) \cup l(q_{3})$, therefore q.psi = false for $q_{2},q_{3}$, therefore q.phi := not(false) = true in these states.

• Case 3: $\phi = \psi_{1} \wedge \psi_{2}$. Call algorithm $docheck(\psi_{1} )$; $docheck(\psi_{2} )$; one has to check for all $q \in Q$ whether q.phi := and(q.psi1, q.psi2).
• Example: $\phi = a \wedge f$. $docheck(a)$ gives q.psi1 = true for $q_{0}, q_{1}, q_{4}$, and q.psi2 = true for $q_{1}, q_{3}, q_{4}$. Because q.phi := and(q.psi1, q.psi2) we get q.phi := true for $\{q_{0}, q_{1}, q_{4}\} \cap \{q_{1}, q_{3}, q_{4}\} = \{q_{1}, q_{4}\}$

• Case 4: $\phi = \textbf{EX} \psi$. Call algorithm $docheck(\psi)$; one has to check for all $(q, q') \in \Delta$ if q'.psi := true then q.phi = true.
• Example: $\phi = \textbf{EX} a \wedge f$. $docheck(a \wedge f)$ which gives us q.psi := true for $\{q_{0}, q_{1}, q_{4}\} \cap \{q_{1}, q_{3}, q_{4}\} = \{q_{1}, q_{4}\}$. Because $q_{1}, q_{4}$ both are successors of $q_{0}$ we can say q.phi = true.

• Case 5: $\phi = \textbf{E} ( \psi_{1} \textbf{U} \psi_{2})$. Call algorithm $docheck(\psi_{1} )$; $docheck(\psi_{2} )$; one has first to check for all q whether q.psi2 = true. If so then a set $L = L + \{q\}$. In a second step -if L is not empty- one has to check whether q.psi1 = true for some $q^{*}$ as chained predecessors of some of the q's of L, if so do q.psi1 = true.
• Example: $\phi = \textbf{E} ( g \textbf{U} f)$. Call $docheck(g )$; $docheck(f)$; which gives us q.psi2 := true for $L = \{q_{1}, q_{3}, q_{4}\}$. Because property g is in $l(q_{0})$ and $q_{0}$ is preceding $q_{1}$ as well as $q_{4}$ q.ps1 = true for at least one case and therefore q.phi = true.

• Case 6: $\phi = \textbf{A} ( \psi_{1} \textbf{U} \psi_{2})$. ....(see exercises below).