Logique temporelle

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
image illustrant la logique image illustrant l’informatique théorique
Cet article est une ébauche concernant la logique et l’informatique théorique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

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.

Définition[modifier | modifier le code]

Dans cet article, seul est présenté le calcul des propositions temporel, autrement dit un calcul des propositions augmenté de modalités temporelles, qui sera néanmoins appelé « logique temporelle ».

Ces logiques sont 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 usuels : 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) (la lettre X vient de l'anglais next : « suivant »)
  • F : un jour (la lettre F vient de l'anglais finally : « finalement »)
  • G : toujours (la lettre G vient de l'anglais globally : « globalement »)
  • U : jusqu'à (la lettre U vient de l'anglais until de même sens)
  • R : release (littéralement « relâcher »)

Une formule de logique des propositions classique, comme 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} (où a a la valeur vrai et b et c ont la valeur faux) rend la formule fausse, le sous-ensemble {b, c} la rend vraie.

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 telle que chaque soit une partie de P. Notons M une telle formule, nous avons :

Table LTL.png

[Sémantique de R à corriger dans l'image ci-dessus :

]

[AUSSI : remplacer par dans la sémantique de U et R (et modifier les interprétations intuitives respectives de U et R ci-dessous en accord) ? Il semble que ce soit la convention usuellement retenue.]

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 à l'étape suivante ;
  • F(f) est vraie maintenant si f est vraie à au moins une étape ultérieure y compris maintenant ;
  • G(f) est vraie maintenant si f est vraie à toutes les étapes suivantes y compris maintenant ;
  • f1 U f2 est vraie si, d'une part, f2 est vraie plus tard ou maintenant et, d'autre part, 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 ou si f2 est tout le temps vraie.

On peut noter que les modalités U et R sont duales l'une de l'autre :

Différentes logiques[modifier | modifier le code]

Il existe différentes logiques temporelles, dont :

Notes et références[modifier | modifier le code]

  1. a et b (en) 0. Maler et D. Nickovic, « Monitoring Temporal Properties of Continuous Signals », dans Y. Lakhnech et S. Yovine, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, vol. 3253, Springer Berlin Heidelberg, (ISBN 978-3-540-23167-7, DOI 10.1007/978-3-540-30206-3_12).

Articles connexes[modifier | modifier le code]