Logique des Arbres de Computation (CTL)

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.