La logique temporelle

La logique temporelle ou modale trouve de nombreuses applications en informatique : traitement du langage naturel, représentation des connaissances, spécification de systèmes [19], etc. Cette logique étend la logique conventionnelle (propositionnelle) en introduisant de nouveaux opérateurs qui permettent de référencer plusieurs instants différents de l’exécution d’un système. La logique temporelle permet ainsi d’exprimer des propriétés dynamiques portant sur plusieurs états des traces d’exécution d’un système. Dans la littérature, nous distinguons les deux classes principales de logique temporelle suivantes : – La logique linéaire comme LTL (Linear Temporal Logic) permettant d’exprimer des propriétés portant sur des chemins individuels issus de l’état initial du programme. – La logique arborescente comme CTL (Computation Tree Logic) permettant d’exprimer des propriétés portant sur les arbres d’exécution issus de l’état initial du programme. Il existe aussi la logique CTL* qui permet de décrire à la fois des propriétés linéaires et arborescentes. La logique CTL* est souvent considérée comme une fusion des logiques LTL et CTL puisque les formules LTL et CTL sont des sous-ensembles des formules CTL*. 2.1.1 La logique LTL LTL est définie sur un ensemble de variables propositionnelles {p, q, .. .}, de connecteurs logiques propositionnels habituels ¬, ∧, ∨, → et de connecteurs temporels (G, F, U et X). La grammaire associée à la logique LTL est comme suit : 19 La logique temporelle – les formules atomiques : ψ, φ := p | q | . . . | true | false – les formules construites à partir de connecteurs propositionnels : ψ := φ | ¬φ | φ ∧ φ | φ ∨ φ | φ ⇒ φ | φ ⇔ φ – les formules construites à partir de connecteurs temporels : – Gφ : (G comme Globally) spécifie que φ est toujours vrai – Fφ : (F comme Futur) indique que φ sera vrai dans le futur – φUψ : (U comme Until) spécifie que φ reste vrai jusqu’à ce que ψ devienne vrai. Cet opérateur impose que le système atteigne un état où ψ devient vrai. – Xφ : (X comme Next) spécifie que φ sera vrai à l’étape suivante de l’exécution 2.1.2 La logique CTL Contrairement à la logique LTL qui considère une vue linéaire du système, la logique CTL (Computation Tree Logic) permet de prendre en compte plusieurs futurs possibles à partir d’un état donné du système. La logique CTL a donc une vision arborescente de l’évolution du système. Elle étend la grammaire de LTL en incluant deux quantificateurs de chemins : l’un universel (A) et un second existentiel (E). – A signifie : « pour tous les chemins possibles de calcul à partir de l’état courant » – E signifie : « pour un certain chemin de calcul à partir de l’état courant » Les formules CTL sont donc toutes précédées des quantificateurs A ou E et sont définies par la grammaire suivante : φ, ψ :=EGφ | EFφ | EφUψ | EXφ | AGφ | AFφ | Aφ U ψ | AXφ avec φ, ψ désignant des formules LTL. La logique CTL introduit également quelques notions d’équité afin de ne considérer que les chemins où aucun événement du système ne prend indéfiniment le contrôle. Par exemple, dans un système d’allocation de ressources partagées par plusieurs utilisateurs, on ne voudrait pas s’intéresser aux chemins où un utilisateur garde la ressource indéfiniment. Pour ce faire, CTL introduit deux opérateurs Af et Ef pour préciser qu’on ne considère que les chemins jugés équitables.

La logique CTL

La logique CTL∗ est la logique temporelle la plus générale. Comme en LTL et CTL, une formule CTL∗ est donc construite à partir de propositions atomiques, de connecteurs propositionnels, de connecteurs temporels et de quantificateurs de chemins. Les opérateurs propositionnels et les quantificateurs de chemins restent les mêmes que dans CTL. Ajouté à ces différents connecteurs, CTL∗ introduit un cinquième connecteur temporel noté W et dont la sémantique est comme suit : étant donné deux prédicats p et q, pWq signifie que p doit rester vrai jusqu’à ce que q soit établi. Contrairement au connecteur U, le connecteur W n’impose pas que le prédicat q devienne vrai durant l’exécution du programme. En CTL∗ , on distingue les formules d’états de celles de chemins : – Une formule d’état φ est définie comme suit : φ := p | ¬φ | φ ∧ φ | φ ∨ φ | Aψ | Eψ avec ψ désignant une formule de chemin. – Une formule de chemin ψ est quant à elle définie par : ψ := φ | ¬ψ | ψ ∧ ψ | ψ ∨ ψ | Xψ | Fψ | Gψ | ψUψ | ψWψ Notons, qu’une nouvelle notation des connecteurs temporels F et G, très utilisée dans la littérature, a été introduite dans la logique CTL∗ . Les connecteurs F et G sont notés ♦ et  respectivement. Ces nouvelles notations s’expriment comme suit : – ♦p=⊤Up signifie que p sera vrai dans le futur. – p=¬♦¬p signifie que p est toujours vrai. Par conséquent, l’opposé de p ne sera jamais vrai dans le futur. 2.2 Vérification de propriétés de vivacité d’UNITY avec Event B Dans [4], les auteurs proposent une méthode de vérification de propriétés de vivacité sur un système spécifié en Event B [2]. Pour ce faire, ils se basent sur l’opérateur LeadsTo défini dans la logique UNITY [18] en distinguant deux classes de propriétés : 1. Propriétés basiques : étant donnés deux prédicats p et q, la propriété p ensures q signifie que le prédicat p reste vérifié tant que le prédicat q ne l’est pas encore. De 21 plus, elle impose que q soit vérifié dans le futur. Cette propriété se décline en deux cas : (a) Propriété basique avec progrès minimum : dans ce cas, on exige que le prédicat q soit vérifié immédiatement sur l’état suivant l’état où le prédicat p est vrai. Cette propriété exige également la possibilité d’évolution du système en tout état qui satisfait p, i.e., il doit toujours exister un événement dont la précondition est vraie. Formellement : p ensures q ≡ (∀t.(p ∧ ¬q ∧ grd.t ⇒ wp.t.q)) ∧ (∃s.(p ∧ ¬q ⇒ grd.s)) avec : – t et s deux événements quelconques du système. – grd.t et grd.s les gardes de t et s respectivement. – wp.t.q représente la plus faible précondition où t termine dans q. (b) Propriété basique avec équité faible : dans ce cas, on n’exige pas que q soit vrai immédiatement sur l’état suivant l’état vérifiant p. Cependant, tous les événements potentiellement exécutables (dont la précondition est vraie) doivent établir q ou préserver p. De plus, il doit toujours exister un événement exécutable qui permet d’établir q. Formellement : p ensures q ≡ (∀t.(p ∧ ¬q ⇒ wp.t.(p ∨ q))) ∧ (∃s.(p ∧ ¬q ⇒ wp.s.q ∧ grd.s)) 2. Propriétés générales : contrairement aux propriétés de base, les propriétés générales n’imposent pas que le prédicat p reste vrai tant que le prédicat q n’est pas vérifié. La preuve d’une propriété de vivacité générale “LeadsTo”, notée p ❀ q, doit être établie en applicant les règles suivantes : – Règle basique (BRL) : si la propriété basique p ensures q est vérifiée alors, nous pouvons déduire que la propriété p ❀ q est aussi vérifiée : p ensures q p ❀ q – Règle de transitivité (TRA) : une propriété générale p ❀ q est vérifiée si cette dernière peut être déduite à partir de plusieurs propriétés plus élémentaires en applicant la transitivité :  Afin donc de pouvoir prouver ces mêmes propriétés en Event B, les auteurs proposent une ré-expression des différentes règles suscitées en termes d’obligations de preuve B. La présentation de ces obligations de preuve fait l’objet des sections suivantes.