## Tuesday, February 5, 2013

### CTL Fixed-point Model Checking With Illustrations

This is a mutual-exclusion protocol for two processes. Here is the tikz model representation. Credit: R. Sebastiani from disi.unitn.it
\begin{tikzpicture}[node distance = 2.5cm]
\tikzstyle{every state}=[fill=none]
\node[state] (a) {N1,N2};
\node[above of=a,yshift=-1cm] {$[C_{1} \wedge C_{2}]$};
\node[state,xshift=-2cm] (b) [below left of=a]{T1,N2};
\node[state,xshift=2cm] (c) [below right of=a]{N1,T2};
\node[state] (d) [below left of=b]{C1,N2};
\node[state] (e) [below right of=b]{T1,T2};
\node[state] (f) [below left of=c]{T1,T2};
\node[state] (g) [below right of=c]{N1,C2};
\node[state] (h) [below right of=d]{C1,T2};
\node[state] (i) [below right of=f]{T1,C2};
\path[->] +(-1,1) edge (a);
\path[->] (a) edge[red] (b) (a) edge (c) (b) edge[red] (d) (b) edge (e) (c) edge[red] (f) (c) edge (g) (d) edge (h) (e) edge[red] (h) (f) edge (i) (g) edge[red] (i);
\draw[->] (i) .. controls +(180:4cm) and +(0:4cm) .. (b);
\draw[->] (h) [red].. controls +(0:4cm) and +(180:4cm) .. (c);
\path[->] (d) edge[red,bend left,out=60] (a);
\path[->] (g) edge[bend right,out=-60] (a);
\end{tikzpicture}

To create a Bezier curve, we add some control points in the path, for instance:
\draw[->] (i) .. controls +(180:4cm) and +(0:4cm) .. (b);

The procedure for checking some CTL properties is illustrated in this pdf file.
• AG¬(C1 ∧ C2 )
• AG(N1 → EFT1)