Algorithmes de Model Checking pour LTL

LTL : Propriété \varphi \in LTL

Idée : Construire un automate qui reconnait tous les \omega mots appartenant à la sémantique de \varphi : \lb\varphi\rb
On a besoin d’un automate capable de reconnaître les mots infinis !

Automate de Büchi généralisé (ABG) : <Q, q_{0}, \ra, \mathcal{F}>

\mathcal{F} = \{\mathcal{F}_{1}, \dots, \mathcal{F}_{k}\} ensemble d’ensembles d’états acceptants.
Un “bon” mot, c’est un mot correspondant à un chemin qui passe infiniment souvent par un état de chaque \mathcal{F}_{i}.

Construire un ABG \mathcal{A}_{\varphi}

L’ensemble d’états Q.
Chaque q \in Q sera associé à un ensemble de sous-formule dans Sf_{\varphi}
q_{0} \subseteq Q contient tous les états associés où \varphi apparaît.
Comment choisir les sous-ensembles de Sf_{\varphi} associés aux états dans Q ?

• Cohérence logique
• Maximalité
• Conformité (par rapport à la sémantique de LTL)

États

Cohérence logique

\begin{aligned} \psi_{1} \wedge \psi_{2} \in q \RA& \psi_{1}, \psi_{2} \in q \\ \neg (\psi_{1} \wedge \psi_{2}) \in q \RA& \neg\psi_{1}\in q \text{ ou } \neg\psi_{2}\in q \\ & \psi_{1} \notin q \text{ ou } \psi_{2} \notin q \\ \psi_{1} \vee \psi_{2} \in q \RA& \psi_{1} \in q \text{ ou } \psi_{2} \in q \\ \neg (\psi_{1} \vee \psi_{2}) \in q \RA& \psi_{1} \notin q \text{ et } \psi_{2} \notin q \\ \psi \in q \RA& \neg \psi \notin q \end{aligned}

Maximalité

Pour chaque \psi \in Sf_{\varphi}, chaque état contient \psi ou \neg\psi

Conformité

• \psi_{1} \text{U} \psi_{2} \in q alors \psi_{1} \in q ou \psi_{2} \in q
• \psi_{1} \text{U} \psi_{2} \in Sf_{\varphi} alors pour tout état q \in Q. \psi_{2}\in q \RA \psi_{1} \text{U} \psi_{2} \in q

Exemple p \text{U} (r \vee s)

Sf_{\varphi}=\{p, \neg p, r, \neg r, s, \neg s, r\vee s, \neg(r\vee s), p \text{U}(r \vee s), \neg()\}

• q_{1} = \{p, r, \neg s, \neg(r\vee s), p \text{U}(r \vee s)\} : maximale, conforme, mais pas cohérent
• q_{2} = \{\neg p\, \neg r, \neg s, \neg(r\vee s), p \text{U}(r \vee s)\} cohérent, maximale, mais pas conforme
• q_{3} = \{p, r, \neg s, r\vee s, p \text{U}(r \vee s)\} cohérent, maximale et conforme

Transitions

On met une transition \begin{aligned}(q, \sigma, q') \in Q \times& 2^{\text{AP}} \times Q \\ &\mathcal{P}(\text{AP}) \\&\hookrightarrow\text{étendue avec les négations des propriétés}\end{aligned} ssi :

• \sigma = q \cap \text{AP} étendue avec les négations des propriétés
• \forall X\phi\in Sf_{\varphi} : X\psi \in q \Leftrightarrow \psi \in q'
• \forall \psi_{1} \text{U} \psi_{2} \in Sf_{\varphi} : \psi_{1}\text{U}\psi_{2}\in q \Leftrightarrow (\psi_{2} \in q \vee (\psi_{1}\in q \wedge \psi_{1}\text{U}\psi_{2}\in q'))

États acceptants

Pour toute sous-formule \psi_{1}\text{U}\psi_{2}\in Sf_{\varphi}
\mathcal{F}_{\psi_{1} \text{U}\psi_{2}} \in \mathcal{F} : \mathcal{F}_{\psi_{1} \text{U}\psi_{2}} = \{q\in Q | \psi_{2} \in q \vee \psi_{1} \text{U} \psi_{2} \notin q\}

Exemple \varphi = \text{X}p

• Sf_{\varphi} = \{p, \neg p, \text{X}p, \neg\text{X}p\}
• q_{1} = \{p, \text{X}p\} q_{2} = \{\neg p, \text{X}p\}
• q_{3} = \{p, \neg\text{X}p\} q_{4} = \{\neg p, \neg\text{X}p\}

Tous les états sont acceptants parce que c’est \text{X}p \text{U true} et tous les états satisfont true.
La complexité est exponentielle sur les sous-systèmes de \varphi.