Une logique temporelle à temps ramifié qui combine des opérateurs temporels avec des quantificateurs de chemin explicites (A pour 'pour tous les chemins', E pour 'il existe un chemin') afin d'exprimer des propriétés sur des arbres de futurs possibles plutôt que sur des chronologies uniques.

Principe

Les formules sont évaluées sur des états d'un système de transitions avec quantification sur les chemins d'exécution : Aφ exige φ sur tout chemin depuis l'état, tandis que Eφ requiert l'existence d'au moins un chemin satisfaisant φ, permettant d'exprimer des comportements ramifiés et des choix.

Démonstration

Pour exprimer « toute requête peut conduire à une garantie d'accord selon un certain ordonnancement », on peut utiliser une formule CTL telle que AG(request -> AF grant) pour dire que sur tous les chemins globalement, si request alors sur tous les futurs il existe finalement un grant ; les model checkers CTL évaluent de telles propriétés d'état sur l'arbre de computation.

Mauvaise application

Confondre CTL avec LTL en écrivant des motifs linéaires en attendant une sémantique par trace, ou mal employer les quantificateurs de chemin (par ex. substituer A et E sans tenir compte de leur portée), ce qui produit des spécifications incorrectes des choix non déterministes.

Conséquence

L'utilisation correcte de CTL permet de spécifier et vérifier des propriétés ramifiées telles que l'inévitabilité sous tous les ordonnancements ou l'existence de chemins de récupération, ce qui le rend adapté au raisonnement sur des systèmes avec non-déterminisme ou concurrence.

Inversion

Le renversement est la logique temporelle linéaire où les propriétés sont affirmées sur des traces individuelles sans quantificateurs de chemin explicites ; certaines propriétés ramifiées exprimables en CTL ne peuvent être capturées en LTL pur et réciproquement.

Limite

CTL restreint le placement des opérateurs temporels en les associant à des quantificateurs de chemin dans des formes syntaxiques précises ; CTL* assouplit ces restrictions, et les extensions en temps réel, probabilistes ou multi-agent sortent du CTL standard sauf si elles y sont ajoutées explicitement.

Tension sémantique

Il existe une tension entre CTL et LTL car certaines propriétés système sont succinctes dans l'un mais pas exprimables dans l'autre ; les praticiens doivent choisir la logique dont la perspective sémantique (ramifiée vs linéaire) s'aligne sur les objectifs de vérification.

Synthèse

CTL est le formalisme temporel à temps ramifié qui enrichit les modalités temporelles par des quantificateurs de chemin afin de raisonner sur l'arbre des exécutions possibles à partir d'un état, permettant d'exprimer des propriétés temporelles universelles et existentielles pour des systèmes à choix.