Logique temporelle

Les différentes logiques temporelles sont des logiques mathématiques et plus précisément des logiques modales. La caractéristique commune de ces logiques est l'ajout de modalités (c'est-à-dire des « transformeurs de prédicats ») permettant de donner une information sur le temps, par exemple, la formule peut se lire : « la formule est satisfaite jusqu'à ce que la formule le soit ».

Intuitivement, cela signifie que la notion de vérité dans ces logiques dépend de l'évolution du monde. C'est-à-dire qu'une proposition peut être, à un moment, fausse, puis plus tard, devenir vraie, etc.

Plusieurs logiques temporelles peuvent être décrites, en fonction des types de modalités de base qu'elles utilisent.

Ces logiques sont très utilisées en vérification formelle, où les techniques mises en œuvre sont essentiellement à base de model checking. On peut, par exemple, y exprimer simplement le fait qu'un événement dangereux ne doit pas arriver tant qu'une certaine condition de sécurité n'est pas satisfaite.

Other Languages
Ελληνικά: Χρονική λογική
日本語: 時相論理
Nederlands: Tijdslogica
português: Lógica temporal
slovenčina: Temporálna logika
中文: 时间逻辑