Un formalisme pour exprimer des propositions sur l'ordre temporel et les propriétés d'états aux points ou intervalles temporels, utilisant des opérateurs temporels tels que 'G' (globalement), 'F' (finalement), 'X' (suivant) et 'U' (jusqu'à).

Principe

Augmenter les langages propositionnels ou prédicatifs par des modalités temporelles interprétées sur un modèle du temps (linéaire ou arboré) de sorte que les formules décrivent comment des vérités persistent, se produisent éventuellement ou se relient au fil de la succession temporelle.

Démonstration

Pour spécifier un programme concurrent, la formule temporelle G(request -> F grant) affirme que sur chaque chronologie d'exécution, chaque fois qu'une requête survient, elle est éventuellement suivie d'un accord ; les outils de model checking utilisent de telles formules pour vérifier les traces du système par rapport à la spécification.

Mauvaise application

Employer une formule temporelle linéaire pour affirmer des propriétés de comportements ramifiés (par ex. supposer que Fφ sur une chronologie implique Fφ sur tous les futurs) ou confondre modalités temporelles avec des contraintes de temps métriques sans horloges ni durées.

Conséquence

Un usage correct de la logique temporelle permet de spécifier précisément des propriétés de vivacité, de sécurité et d'équité dans le temps et facilite la vérification automatique en traduisant le comportement en modèles temporels vérifiables.

Inversion

Le renversement est la logique atemporelle où les propositions sont évaluées sans structure temporelle et ne peuvent exprimer ni ordre ni éventualité ; les relations temporelles se réduisent à des valeurs de vérité ordinaires dans un état statique unique.

Limite

La logique temporelle, telle que définie classiquement, n'encode pas de façon intrinsèque le minutage métrique réel (sauf extensions vers des logiques temporelles en temps réel) et ne modélise pas les probabilités ; elle présuppose une structure temporelle choisie (discrète/continue, linéaire/ramifiée) qui limite l'expressivité.

Tension sémantique

Il existe une tension entre interprétations linéaires et ramifiées : la logique temporelle linéaire (LTL) évalue les formules sur des chronologies uniques, tandis que les logiques ramifiées (CTL, CTL*) autorisent la quantification sur les chemins ; le choix influe sur les propriétés exprimables et vérifiables.

Synthèse

La logique temporelle fournit un langage et une sémantique pour dire comment des propriétés évoluent ou tiennent dans le temps en ajoutant des opérateurs temporels aux logiques usuelles, permettant de raisonner formellement sur les séquences et les motifs d'états des systèmes et processus.