CTL*

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

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[modifier | modifier le code]

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[réf. souhaitée]. Ceci est surprenant[pourquoi ?], 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[modifier | modifier le code]

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

est une proposition atomique ;
.

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

Sémantique[modifier | modifier le code]

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

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 :

  • indique que sera vérifiée dans tous les calculs possibles ;
  • indique que l'on peut trouver un calcul tel que soit vérifiée ;
  • indique que sera vérifiée dès l'étape suivante du calcul ;
  • indique que sera vérifiée dans la suite du calcul, jusqu'à ce que soit vraie.

Formules d'état[modifier | modifier le code]

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

  1. toujours ;
  2. si et seulement si décore  ;
  3. si et seulement si ;
  4. si et seulement si et  ;
  5. si et seulement si pour tout chemin commençant en  ;
  6. si et seulement si pour au moins un chemin commençant en .

Formules de chemin[modifier | modifier le code]

On note lorsqu'un chemin d'une structure de Kripke satisfait une formule de chemin . Notons également le sous-chemin . Cette relation de satisfaction est définie inductivement par les règles suivantes :

  1. si et seulement si  ;
  2. si et seulement si ;
  3. si et seulement si et  ;
  4. si et seulement si  ;
  5. si et seulement si tel que et on a .

Modalités supplémentaires[modifier | modifier le code]

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

  •  ;
  • .

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

Exemples de formules[modifier | modifier le code]

  • Formule CTL* qui n'est ni dans LTL, ni dans CTL :
  • Formule LTL qui n'est pas dans CTL :
  • Formule CTL qui n'est pas dans LTL :
  • Formule CTL* qui est dans CTL et LTL :

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

Problèmes de décision[modifier | modifier le code]

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[modifier | modifier le code]

  1. a et b Christel Baier et Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, (ISBN 026202649X, lire en ligne)
  2. « delivery.acm.org/10.1145/30000/22173/p240-vardi.pdf?ip=131.254.16.137&id=22173&acc=ACTIVE%2520SERVICE&key=7EBF6E77E86B478F%252E9BD6B3DBCD4B0A3B%252E4D4702B0C3E38B35%252E4D4702B0C3E38B35&CFID=839922977&CFTOKEN=84681748&__acm__=1474297820_4861bc9e061d390bb22019e6bb75c206 », {{Article}} : paramètre « périodique » manquant, paramètre « date » manquant (DOI 10.1145/30000/22173/p240-vardi.pdf, lire en ligne)

Bibliographie[modifier | modifier le code]

  • (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, no 1,‎ , p. 151-178 (DOI http://doi.acm.org/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[modifier | modifier le code]

Articles connexes[modifier | modifier le code]

Liens externes[modifier | modifier le code]