Logique temporelle

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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 (sorte de "constructeurs") permettant de donner une information sur le temps, par exemple, la formule \phi U \psi peut se lire : "la formule \phi est vérifiée jusqu'à ce que la formule \psi 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.

On parle de plusieurs logiques temporelles car on peut utiliser plusieurs types de modalités.

Ces logiques sont très utilisées en vérification formelle, c'est le plus souvent ce genre de formules que l'on cherche à vérifier dans le model checking. On peut, par exemple, exprimer simplement le fait qu'un événement dangereux ne doit pas arriver tant qu'une certaine condition de sécurité n'est pas vérifiée.

Définition[modifier | modifier le code]

Ces logiques sont donc définies sur un ensemble de propositions atomiques P ou variables de propositions. Ces propositions atomiques sont combinées par un certain nombre de connecteurs logiques, dont les connecteurs classiques : et, ou, non, implication, ainsi que d'autres opérateurs que l'on appelle des modalités. La logique temporelle est donc une logique modale. Dans le cas de la logique temporelle linéaire (LTL), on ajoute les modalités suivantes

  • X : demain ou immédiatement après (à distinguer donc du don't care en logique classique noté aussi X)
  • F : un jour
  • G : toujours
  • U : jusqu'à
  • R : release

Une formule de logique des propositions classique, comme par exemple la formule (a et b) ou c sur l'ensemble de propositions P={a,b,c}, associe une valeur de vérité, vrai ou faux, à chaque sous-ensemble de P. Par cette formule exemple, le sous-ensemble {a} est faux, le sous-ensemble {b,c} est vrai.

Une formule de logique temporelle associe une valeur de vérité non pas à chaque partie de P, mais selon le type de logique, à chaque suite de parties de P ou à chaque arbre sur les parties de P. Une logique définie sur les suites est dite linéaire, tandis qu'une formule définie sur les arbres est dite branching logic ou logique à embranchements.

Prenons le cas des logiques linéaires. Une telle logique associe donc une valeur de vérité, vrai ou faux, à chaque suite V = (V_1,V_2,\ldots) telle que chaque V_i soit une partie de P. Notons M une telle formule, nous avons :

Table LTL.png

Intuitivement, si la suite V représente l'évolution dans le temps des différentes propositions de P, alors

  • X(f) est vraie maintenant si f est vraie à partir de l'étape suivante,
  • F(f) est vraie maintenant si f est vraie à au moins une étape ultérieure,
  • G(f) est vraie maintenant si f est vraie à toutes les étapes suivantes y compris maintenant,
  • f1 U f2 est vraie si f1 est vraie (y compris) jusqu'à ce que f2 soit vraie,
  • f1 R f2 est vraie si f2 est vraie (y compris) jusqu'à ce que f1 soit vraie.

Différentes logiques[modifier | modifier le code]

Il existe différentes logiques temporelles, dont :

  • CTL*, une logique arborescente
  • Computation tree logic (en) (CTL), une logique arborescente incluse dans CTL*.
  • Linear temporal logic (en) (LTL), une logique linéaire incluse dans CTL*.
  • Metric Interval Temporal Logic (MITL) qui considère un temps continu et renvoie une valeur booléenne [ref: Maler,Nickovic,2004, monitoring temporal properties of continuous signals]
  • Signal Temporal Logic (STL) qui considère un temps continu et renvoie une valeur réelle [ref: Maler,Nickovic,2004, monitoring temporal properties of continuous signals]

Articles connexes[modifier | modifier le code]