Logique temporelle
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

Les différentes logiques temporelles sont des logiques de propositions ; elles 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 (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) 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 (Les différentes logiques temporelles sont des logiques de propositions ; elles sont donc définies sur un ensemble de propositions atomiques P ou variables de propositions. Ces propositions...) est donc une logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et...) 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 (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui...) de propositions P={a,b,c}, associe une valeur de vérité (La notion de valeur de vérité consiste à attribuer aux énoncés des valeurs numériques au travers de fonctions dont il faudra définir les règles de...), vrai ou faux, à chaque sous-ensemble (En mathématiques, un ensemble A est un sous-ensemble ou une partie d’un ensemble B, ou encore B est sur-ensemble de A, si tout élément du...) 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 (Un arbre est une plante terrestre capable de se développer par elle-même en hauteur, en général au delà de sept mètres. Les...) 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 Vi soit une partie de P. Notons M une telle formule, nous avons :

Image:Table LTL.png

Intuitivement, si la suite V représente l'évolution dans le temps (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.) 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.
Page générée en 0.033 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique