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.

HistoriqueModifier

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.

SyntaxeModifier

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émantiqueModifier

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'étatModifier

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 cheminModifier

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émentairesModifier

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 formulesModifier

  • Formule CTL* qui n'est ni dans LTL, ni dans CTL :  
  • Formule CTL qui n'est pas dans LTL :  
  • 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écisionModifier

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

Notes et référencesModifier

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

BibliographieModifier

  • (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 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 aussiModifier

Articles connexesModifier

Liens externesModifier