Logique temporelle
Un article de Freepedia.
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 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 témporelle 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 un 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 <math>V = (V_1,V_2,\ldots)</math> telle que chaque <math>V_i</math> soit une partie de P. Notons M une telle formule, nous avons :
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.
Exemple historique : latch et clamp
Dans les premières versions de fortran, les espaces hors libellés n'étaient pas significatifs, ce qui créait des difficultés à l'analyseur syntaxique : comment savoir si GOTO5 est le nom d'une variable (GOTO5=.FALSE.) ou un ordre de branchement à l'étiquette 5 ? Comment savoir si DO1I=1 est l'affectation à une variable ou le début d'un ordre de boucle ? On ne le saura qu'en lisant la suite de la ligne.
Le compilateur effectuait donc ce qu'on nommait un latch : prendre une hypothèse, mais garder le contexte à tout hasard pour revenir en arrière en cas d'imprévu. Lorsque la lecture de la suite levait l'indétermination et que la prévision était bonne, on effectuait un clamp pour annuler le latch. Dans le cas contraire, on revenait au point de décision avec une information indiquant que la première hypothèse n'était pas la bonne. Ces techniques sont devenues inutiles à mesure que l'on a construit des langages plus logiquement et qu'on a mis à ces nouvelles normes les langages plus anciens.
