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)