CTL*

En informatique théorique, notamment en vérification formelle, CTL* (prononcé CTL star en anglais) est une logique temporelle. C'est une généralisation de la logique du temps arborescent (en) (CTL : computation tree logic) et de la logique temporelle linéaire (LTL : linear temporal logic). Elle combine librement les quantificateurs sur chemins et les opérateurs temporels. CTL* est de ce fait une logique arborescente. La sémantique des formules CTL* repose sur une structure de Kripke.

Historique

La logique temporelle linéaire (LTL) a d'abord été proposée par Amir Pnueli en 1977, dans le but de vérifier des programmes informatiques. Quatre ans plus tard, en 1981, Edmund M. Clarke et Allen Emerson inventent CTL et le model checking. CTL* fut définie par Emerson et Joseph Y. Halpern en 1986.

Il est intéressant de noter que CTL et LTL ont été développées indépendamment, avant CTL*. Ces deux logiques sont devenues très importantes au sein de la communauté du model checking, alors que CTL* reste peu utilisée. Ceci est surprenant, car la complexité algorithmique du model checking CTL* n'est pas pire que celle du model checking LTL : ces deux problèmes sont dans PSPACE.

Syntaxe

Le langage des formules CTL* est généré par la grammaire hors contexte suivante :

{\displaystyle \Phi

où

p

est une proposition atomique ;

{\displaystyle \phi

Les formules CTL* valides sont construites en utilisant le symbole $\Phi$ . Ces formules sont appelées formules d'état, alors que celles créées en utilisant le symbole $\phi$ sont appelées formules de chemin.

Sémantique

La sémantique de CTL* est interprétée dans une structure de Kripke. Les états sont décorés par les propositions atomiques $p$ .

CTL* permet de raisonner à la fois sur les étapes de calcul (à travers les formules d'états interprétées par rapport aux états) et les calculs dans leur ensemble (avec les formules de chemins interprétées sur les chemins).

On peut donner la sémantique intuitive suivante :

$A\phi$ indique que $\phi$ sera vérifiée dans tous les calculs possibles ;
$E\phi$ indique que l'on peut trouver un calcul tel que $\phi$ soit vérifiée ;
$X\phi$ indique que $\phi$ sera vérifiée dès l'étape suivante du calcul ;
$\phi _{1}U\phi _{2}$ indique que $\phi _{1}$ sera vérifiée dans la suite du calcul, jusqu'à ce que $\phi _{2}$ soit vraie.

Formules d'état

On note $s\models \Phi$ lorsqu'un état $s$ d'une structure de Kripke satisfait une formule d'état $\Phi$ . Cette relation est définie inductivement par les règles suivantes :

$({\mathcal {M}},s)\models \top$ toujours ;
$({\mathcal {M}},s)\models p$ si et seulement si $p$ décore $s$ ;
$({\mathcal {M}},s)\models \neg \Phi$ si et seulement si $({\mathcal {M}},s)\not \models \Phi$ ;
$({\mathcal {M}},s)\models \Phi _{1}\land \Phi _{2}$ si et seulement si $({\mathcal {M}},s)\models \Phi _{1}$ et $({\mathcal {M}},s)\models \Phi _{2}$ ;
$({\mathcal {M}},s)\models A\phi$ si et seulement si $\pi \models \phi$ pour tout chemin $\ \pi$ commençant en $s$ ;
$({\mathcal {M}},s)\models E\phi$ si et seulement si $\pi \models \phi$ pour au moins un chemin $\ \pi$ commençant en $s$ .

Formules de chemin

On note $\pi \models \phi$ lorsqu'un chemin $\pi =s_{0}\to s_{1}\to \cdots$ d'une structure de Kripke satisfait une formule de chemin $\phi$ . Notons également $\ \pi [n]$ le sous-chemin $s_{n}\to s_{n+1}\to \cdots$ . Cette relation de satisfaction est définie inductivement par les règles suivantes :

$({\mathcal {M}},\pi )\models \Phi$ si et seulement si $({\mathcal {M}},s_{0})\models \Phi$ ;
$({\mathcal {M}},\pi )\models \neg \phi$ si et seulement si $({\mathcal {M}},\pi )\not \models \phi$ ;
$({\mathcal {M}},\pi )\models \phi _{1}\land \phi _{2}$ si et seulement si $({\mathcal {M}},\pi )\models \phi _{1}$ et $({\mathcal {M}},\pi )\models \phi _{2}$ ;
$({\mathcal {M}},\pi )\models X\phi$ si et seulement si $({\mathcal {M}},\pi [1])\models \phi$ ;
$({\mathcal {M}},\pi )\models (\phi _{1}U\phi _{2})$ si et seulement si $\exists n\geqslant 0$ tel que $({\mathcal {M}},\pi [n])\models \phi _{2}$ et $\forall 0\leqslant k<n$ on a $({\mathcal {M}},\pi [k])\models \phi _{1}$ .

Modalités supplémentaires

On peut définir les modalités $F$ (« arrivera au moins une fois dans le futur ») et $G$ (« arrivera tout le temps dans le futur ») de la manière suivante :

$F\phi \equiv \top U\phi$ ;
$G\phi \equiv \neg F\neg \phi$ .

Notons qu'elles s'appliquent à des formules de chemin.

Exemples de formules

Formule CTL* qui n'est ni dans LTL, ni dans CTL : $EX(p)\land AFG(p)$
Formule CTL qui n'est pas dans LTL : $AFG(p)$
Formule CTL qui n'est pas dans LTL : $EX(p)$
Formule CTL* qui est dans CTL et LTL : $AG(p)$

Remarque : lorsque l'on considère LTL comme un sous-ensemble de CTL*, toute formule de LTL est implicitement préfixée du quantificateur universel de chemin $A.$

Problèmes de décision

Le model checking de CTL* est PSPACE-complet[1] et le problème de satisfiabilité est 2EXPTIME-complet[1] - [2].

Notes et références

Christel Baier et Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 1^er janvier 2008, 975 p. (ISBN 978-0-262-02649-9 et 0-262-02649-X, lire en ligne)
(en) Orna Kupferman et Moshe Y. Vardi, « Church’s problem revisited », Bulletin of Symbolic Logic, vol. 5, n^o 2,‎ juin 1999, p. 245-263 (DOI 10.2307/421091, lire en ligne)

Bibliographie

(en) Amir Pnueli, « The Temporal Logic of Programs », Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. DOI= 10.1109/SFCS.1977.32 (lire en ligne [PDF])
(en) E. Allen Emerson et Joseph Y. Halpern, « “Sometimes” and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic », Journal of the ACM, vol. 33, n^o 1,‎ janvier 1986, p. 151-178 (DOI 10.1145/4904.4999, lire en ligne [PDF])
(en) Philippe Schnoebelen, « The Complexity of Temporal Logic Model Checking ». Advances in Modal Logic 2002 : 393–436 (lien en ligne [PDF])

Voir aussi

Liens externes

(en) Diapositives d'enseignement sur CTL du professeur Alessandro Artale à l'université libre de Bolzano

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.