Voir la source de CTL*

En [[informatique théorique]], notamment en [[vérification formelle]], '''CTL*''' (prononcé ''{{Langue|en|CTL star}}'' en anglais) est une [[logique temporelle]]. C'est une généralisation de la {{Lien|langue=en|trad=Computation tree logic|fr=logique du temps arborescent}} (CTL : ''{{Langue|en|computation tree logic}}'') et de la [[logique temporelle linéaire]] (LTL : ''{{Langue|en|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{{Référence souhaitée|}}. Ceci est surprenant{{Pourquoi|}}, car la [[Théorie de la complexité (informatique théorique)|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 formel|langage]] des formules CTL* est généré par la [[grammaire hors contexte]] suivante :

:<math>\Phi::=\top  \mid p \mid \neg\Phi \mid (\Phi\land\Phi) \mid A\phi \mid E\phi</math> où <math>p</math> est une [[formule atomique|proposition atomique]] ;
:<math>\phi::=\Phi \mid \neg\phi \mid (\phi\land\phi) \mid  X\phi \mid (\phi U \phi)
</math>.

Les formules CTL* valides sont construites en utilisant le symbole <math>\Phi</math>. Ces formules sont appelées ''formules d'état'', alors que celles créées en utilisant le symbole <math>\phi</math> 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 <math>p</math>.

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 :
* <math>A \phi</math> indique que <math>\phi</math> sera vérifiée dans tous les calculs possibles ;
* <math>E \phi</math> indique que l'on peut trouver un calcul tel que <math>\phi</math> soit vérifiée ;
* <math>X \phi</math> indique que <math>\phi</math> sera vérifiée dès l'étape suivante du calcul ;
* <math>\phi_1 U \phi_2</math> indique que <math>\phi_1</math> sera vérifiée dans la suite du calcul, jusqu'à ce que <math>\phi_2</math> soit vraie.

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

# <math>(\mathcal{M}, s) \models \top</math> toujours ;
# <math>(\mathcal{M}, s) \models p</math> si et seulement si <math>p</math> décore <math>s</math> ;
# <math>(\mathcal{M}, s) \models \neg\Phi</math> si et seulement si<math>(\mathcal{M}, s) \not\models \Phi</math> ;
# <math>(\mathcal{M}, s) \models \Phi_1 \land \Phi_2</math> si et seulement si <math>(\mathcal{M}, s) \models \Phi_1 </math> et <math>(\mathcal{M}, s) \models \Phi_2 </math> ;
# <math>(\mathcal{M}, s) \models A\phi</math> si et seulement si <math>\pi\models\phi</math> pour tout chemin <math>\ \pi</math> commençant en <math>s</math> ;
# <math>(\mathcal{M}, s) \models E\phi</math> si et seulement si <math>\pi\models\phi</math> pour au moins un chemin <math>\ \pi</math> commençant en <math>s</math>.

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

# <math>(\mathcal{M}, \pi) \models \Phi</math> si et seulement si <math>(\mathcal{M}, s_0) \models \Phi</math> ;
# <math>(\mathcal{M}, \pi) \models \neg\phi</math> si et seulement si<math>(\mathcal{M}, \pi) \not\models \phi</math> ;
# <math>(\mathcal{M}, \pi) \models \phi_1 \land \phi_2</math> si et seulement si <math>(\mathcal{M}, \pi) \models \phi_1 </math> et <math>(\mathcal{M}, \pi) \models \phi_2 </math> ;
# <math>( \mathcal{M}, \pi) \models X\phi</math> si et seulement si <math>(\mathcal{M}, \pi[1]) \models \phi</math> ;
# <math>(\mathcal{M}, \pi) \models (\phi_1U\phi_2)</math>si et seulement si <math>\exists n\geqslant 0</math> tel que <math>(\mathcal{M},\pi[n]) \models\phi_2 </math> et <math>\forall 0\leqslant k < n</math> on a <math>(\mathcal{M},\pi[k]) \models \phi_1</math>.

== Modalités supplémentaires ==
On peut définir les modalités <math>F</math> (« arrivera au moins une fois dans le futur ») et <math>G</math> (« arrivera tout le temps dans le futur ») de la manière suivante :
* <math>F \phi \equiv \top U \phi</math> ;
* <math>G \phi \equiv \neg F \neg \phi</math>.
Notons qu'elles s'appliquent à des formules de chemin.

== Exemples de formules ==
* Formule CTL* qui n'est ni dans LTL, ni dans CTL : <math>EX(p) \land AFG(p)</math>
* Formule CTL qui n'est pas dans LTL : <math>AFG(p)</math>
* Formule CTL qui n'est pas dans LTL : <math>EX(p)</math>
* Formule CTL* qui est dans CTL et LTL : <math>AG(p)</math>

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 <math>A.</math>

== Problèmes de décision ==
Le [[model checking]] de CTL* est PSPACE-complet<ref name=":0">{{Ouvrage|prénom1=Christel|nom1=Baier|prénom2=Joost-Pieter|nom2=Katoen|titre=Principles of Model Checking (Representation and Mind Series)|éditeur=The MIT Press|date=2008-01-01|pages totales=975|isbn=978-0-262-02649-9|isbn2=0-262-02649-X|lire en ligne=http://dl.acm.org/citation.cfm?id=1373322}}</ref> et le problème de satisfiabilité est 2EXPTIME-complet<ref name=":0" />{{,}}<ref>{{article | langue=en | auteur1=[[Orna Kupferman]] | auteur2=[[Moshe Y. Vardi]] |titre=Church’s problem revisited | périodique=Bulletin of Symbolic Logic | mois=juin | année=1999 | volume=5 | numéro=2 | lire en ligne=https://www.jstor.org/stable/421091?seq=1#page_scan_tab_contents | doi=10.2307/421091 | passage=245-263}}</ref>.

== Notes et références ==
<references />

== Bibliographie ==
* {{en}} [[Amir Pnueli]], « {{Langue|en|The Temporal Logic of Programs}} », {{Langue|en|Proceedings of the 18th Annual Symposium on Foundations of Computer Science}} (FOCS), 1977, 46–57. DOI= 10.1109/SFCS.1977.32 <small>([http://fi.ort.edu.uy/innovaportal/file/20124/1/49-pnueli_temporal_logic_of_programs.pdf lire en ligne] {{pdf}})</small>
* {{article
| langue        = en
| auteur1       = E. Allen Emerson
| auteur2       = Joseph Y. Halpern
| titre         = “Sometimes” and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic
| périodique    = [[Journal of the ACM]]
| volume        = 33
| numéro        = 1
| passage       = 151-178
| date          = Janvier 1986
| lire en ligne = http://www.cs.utah.edu/~ritwik/papers/emerson.pdf
| format        = pdf
| doi           = 10.1145/4904.4999}}
* {{en}} Philippe Schnoebelen, « {{Langue|en|The Complexity of Temporal Logic Model Checking}} ». {{Langue|en|Advances in Modal Logic 2002}} : 393–436 <small>([http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf lien en ligne] {{pdf}})</small>

== Voir aussi ==
=== Articles connexes ===

* [[Logique temporelle]]
* [[Structure de Kripke]]
* [[Model checking]]

=== Liens externes ===
* {{en}} [http://www.inf.unibz.it/~artale/FM/slide4.pdf Diapositives d'enseignement sur CTL] du professeur [[Alessandro Artale]] à l'[[université libre de Bolzano]]

{{Portail|logique|informatique théorique}}

[[Catégorie:Logique modale]]
[[Catégorie:Vérification de modèles]]
[[Catégorie:Logique temporelle]]