\varphi = p \text{U} r
Q = \begin{aligned}\{&\{p, r, p \text{U} r\}, \{p, \neg r, p \text{U} r\}, \{\neg p, r, p \text{U} r\}, \\ &\{\neg p, \neg r, p \text{U} r\}, \{p, r, \neg(p \text{U} r)\}, \{p, \neg r, \neg(p \text{U} r)\}, \\ &\{\neg p, r, \neg(p \text{U} r)\}, \{\neg p, \neg r, \neg(p \text{U} r)\}\}\end{aligned}
On retire ceux qui sont non-conforme :
Q = \{\{p, r, p \text{U} r\}, \{p, \neg r, p \text{U} r\}, \{\neg p, r, p \text{U} r\}, \{p, \neg r, \neg(p \text{U} r)\}, \{\neg p, \neg r, \neg(p \text{U} r)\}\}

dessin

En pratique : S \overset{?}{\vDash} \varphi

Construire \mathcal{A}_{\neg \varphi}
\mathcal{L}(S) \cap \mathcal{A}_{\neg \phi} \overset{?}{=} \varnothing avec \mathcal{A}_{\neg \phi} : Q de taille exponentielle à |\varphi| et \cap le produit des STEs.

Complexité d’algo : PSPACE-Complet

\begin{aligned} \neg(P\ \text{U}R) &\nLeftrightarrow \neg P\ \text{U}\neg R \\ \neg(P\ \text{U}R) &= G(\neg r) \vee \neg r\ \text{U} (\neg p \wedge \neg r) \end{aligned}

Algorithmes de model checking pour CTL

Pour chaque état q \in Q, dédier un champ q\varphi \in \B (\in \{\top, \bot\})
Procédure marquage (\varphi) :
\begin{aligned} \text{Cas }& \varphi = P : \\ \quad& \text{Pour } q \in Q \\ &\quad q.\varphi \leftarrow P\in\mathcal{L}(q) \end{aligned}

\begin{aligned} \text{Cas }& \varphi = \neg\psi : \\ \quad& \text{Pour } q \in Q \\ &\quad q.\varphi \leftarrow \neg q.\psi \end{aligned}
\begin{aligned} \text{Cas }& \varphi = \psi_{1} \wedge \psi_{2} : \\ \quad& \text{Marquage(}\psi_{1}\text{), Marquage(}\psi_{2}\text{)} \\ \quad& \text{Pour } q \in Q \\ &\quad q.\varphi \leftarrow q.\psi_{1} \wedge q.\psi_{2} \end{aligned}
\begin{aligned} \text{Cas }& \varphi = \psi_{1} \wedge \psi_{2} : \\ \quad& \text{Marquage(}\psi\text{)} \\ \quad& \text{Pour } q \in Q \\ &\quad q.\varphi \leftarrow \bot \\ &\quad \text{Pour } q\ra q' \in \ra \\ &\qquad \text{Si } q' \psi = \top \\ &\quad\qquad q.\varphi \leftarrow \top \end{aligned}
\begin{aligned} \text{Cas }& \varphi = \text{AX}.\psi \quad \neg\text{EX}\neg\varphi : \\ \quad& \text{Cas } \varphi = \psi_{1}\text{EU}\psi_{2} \\ &\qquad \text{Marquage(}\psi_{1}\text{), Marquage(}\psi_{2}\text{)} \\ &\qquad \text{Pour } q \in Q \\ &\quad\qquad q.\varphi \leftarrow \bot \\ &\qquad \text{QU} \leftarrow \varnothing \\ &\qquad \text{Pour } q \in Q \\ &\quad\qquad \text{Si } q.\phi_{2} = \top \\ &\qquad\qquad \text{QU} \leftarrow \text{QU U}\{q\} \\ &\qquad\qquad q.\varphi \leftarrow \top \\ \quad& \text{Tant que QU} \neg \varnothing\\ &\qquad \text{Piocher } q \in\text{QU} \\ &\qquad \text{Pour } q' \ra q \in \ra \\ &\quad\qquad \text{Si } q'.\psi_{1} = \top \wedge q'.\varphi = \bot \\ &\qquad\qquad \text{QU} \leftarrow \text{QU U}\{q'\} \\ &\qquad\qquad q'.\psi\leftarrow \top \\ &\qquad \text{QU} \leftarrow \text{QU} \backslash\{q\} \end{aligned}

Exercice

Cas : \varphi = \psi_{1}\text{AU}\psi_{2}

Complexité

O(|\varphi|.(|Q|+|\ra|))
\RA Complexité polynomiale