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 (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. 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. Le langage des formules CTL* est généré par la grammaire hors contexte suivante : où 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. 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.