Exercices de Logique Temporelle

Exercice 1 (Principal 2015)

Question 1 - Évaluation des formules dans l'état courant

Nous évaluons ici des formules de logique temporelle linéaire (LTL) à partir de l'état courant d'une exécution.

• Fp est-il vrai si p est vrai tout de suite dans l’état courant ? Réponse : Oui. Explication : L'opérateur F (Future ou ◊) signifie qu'une propriété doit être vraie à un moment donné du chemin (maintenant ou plus tard). Si p est vrai dans l'état courant, Fp est immédiatement satisfait.

• Gp est-il vrai si p est faux dans l’état courant et vrai partout ailleurs ? Réponse : Non. Explication : L'opérateur G (Globally, Toujours ou □) exige que la propriété p soit vraie dans tous les états du chemin, sans exception, y compris l'état initial. Puisque p est faux dès le premier état, Gp est faux.

• pUq est-il vrai si p est faux et q est vrai dans l’état courant ? Réponse : Oui. Explication : L'opérateur U (Until ou Jusqu'à) exige que p soit vrai dans tous les états précédant celui où q devient vrai. Si q est vrai dès le départ, il n'y a aucun état strictement précédent. La condition est satisfaite de façon triviale.

• pUq est-il vrai si q est toujours faux, et p est toujours vrai ? Réponse : Non. Explication : Il s'agit ici du "Until" fort, qui impose que l'événement de droite (q) finisse obligatoirement par se produire. Puisque q n'est jamais vrai, la formule n'est pas satisfaite, même si p est vrai pour l'éternité.

Question 2 - Expression des propriétés en logique arborescente (CTL)

La logique arborescente (CTL) utilise des quantificateurs de chemin (A pour "All" / tous les chemins, E pour "Exists" / il existe au moins un chemin) couplés aux opérateurs temporels classiques.

• P2. Quelque soit l’état, on finit par aller à un état où p est vrai. Formule : AGAFp Explication : "Quelque soit l'état" se traduit par AG (sur tous les chemins, dans tous les états). "On finit par aller" se traduit par AF (sur tous les chemins futurs partant de cet état, on rencontre p).

• P3. Quelque soit l’état, on peut aller à un état où p est vrai. Formule : AGEFp Explication : Le début reste AG (pour tout état accessible). "On peut aller" indique une possibilité, donc il existe au moins un chemin menant à p, ce qui se traduit par EF (Exists a path where Finally p).

Question 3 - Modèle Kripke pour la propriété P2

Pour satisfaire P2 (AGAFp), il faut que depuis n'importe quel état du système, toutes les exécutions possibles finissent par traverser un état où p est vrai.

Modèle proposé (Automate Kripke) : Imaginons un modèle à 3 états (S0, S1, S2).

• S0 : état initial, p est faux. Transition vers S1.
• S1 : p est faux. Transition vers S2.
• S2 : p est vrai. Transition vers S0.

Dans ce modèle en boucle (S0 → S1 → S2 → S0 → ...), peu importe l'état de départ, on atteindra toujours l'état S2 où p est vrai. La source suggère une suite linéaire p → p → p, qui fonctionne également : un système composé d'un seul état où p est vrai et bouclant sur lui-même (S0, p=vrai, transition S0 → S0) valide AGAFp de manière triviale.

Question 4 - Modèle Kripke pour la propriété P3

Pour satisfaire P3 (AGEFp), il faut que de n'importe quel état, il existe au moins un chemin permettant de rejoindre un état où p est vrai, mais ce n'est pas obligatoire pour tous les chemins (contrairement à P2).

Modèle proposé (Automate Kripke) : Imaginons un modèle à 2 états (S0, S1).

• S0 : p est vrai. Transitions possibles vers S0 et vers S1.
• S1 : p est faux. Transitions possibles vers S0 et vers S1.

Ici, quel que soit l'état où l'on se trouve, il existe une transition menant à S0 (où p est vrai). Cependant, il est aussi possible de rester indéfiniment dans S1 (où p est faux). La propriété AGEFp est satisfaite, mais AGAFp ne le serait pas.

Exercice 2 (Principal 2014)

Note de lecture : Le symbole "" présent dans la source de l'examen est un artefact classique de conversion PDF, remplaçant le symbole carré □ utilisé pour l'opérateur "Toujours" (G ou Globally). Dans la correction, nous utiliserons le symbole  pour respecter les notations de la source, mais gardez à l'esprit qu'il signifie "Toujours".

Question 1 - Formulation de la propriété en logique PLTL

Propriété : À chaque fois que X est vrai, Z devient vrai et restera vrai jusqu’à ce que Y le devienne et Y deviendra inévitablement vrai à un état futur. Formule PLTL : (X → (Z U Y)) Explication : L'opérateur  (Toujours) englobe la condition. Si X est vrai, cela implique (→) que Z doit être vrai jusqu'à l'occurrence de Y (Z U Y). L'utilisation de l'opérateur "Until" (U) fort inclut intrinsèquement le fait que Y finira inévitablement par devenir vrai.

Question 2 - Formalisation de la propriété en logique arborescente CTL

En logique CTL, nous devons ajouter les quantificateurs de chemin ∀ (ou A) pour "tous les chemins". Formule CTL : ∀(X → ∀(Z U Y)) Explication : Dans la syntaxe CTL classique (CTL de base), cette formule s'écrirait AG(X → A[Z U Y]). La notation de l'examen utilise ∀ pour AG (pour tout chemin, toujours) et ∀(Z U Y) pour A[Z U Y] (sur tous les futurs possibles, Z jusqu'à Y).

Question 3 - Construction de la structure de Kripke (Automate)

Variables considérées : X : "timeout" Z : "avertissement" Y : "rejet ou réponse"

Modèle construit : Nous devons concevoir un système où l'apparition d'un "timeout" force le système à afficher un "avertissement" et à le maintenir jusqu'à obtenir un "rejet" ou une "réponse".

• État initial (S0) : État d'attente normal (ni X, ni Y, ni Z).
• État de timeout (S1) : {X, Z} (Timeout et Avertissement sont vrais).
• État d'attente prolongée (S2) : {Z} (L'avertissement reste vrai en attendant la résolution).
• État de résolution (S3) : {Y} (Réponse ou rejet, l'avertissement Z n'est plus obligatoire).

Transitions : S0 → S1 (si timeout), S1 → S2, S2 → S2 (boucle d'attente), S2 → S3 (résolution), S1 → S3 (résolution immédiate après timeout). Toute trace passant par X garantit l'apparition de Y, avec Z maintenu entre-temps.

Question 4 - Trace d'exécution de l'algorithme de model checking CTL

L'algorithme de "model checking" CTL procède par étiquetage ascendant (bottom-up) des états. Pour vérifier ∀(X → ∀(Z U Y)) sur l'automate défini à la question 3 :

1. Étiquetage des propositions atomiques : L'algorithme marque les états contenant X, Z, et Y (par exemple, S3 reçoit l'étiquette Y, S1 reçoit X et Z, S2 reçoit Z).
2. Traitement de ∀(Z U Y) : On identifie les états d'où partent exclusivement des chemins satisfaisant "Z jusqu'à Y".
   • S3 est étiqueté ∀(Z U Y) car Y y est vrai.
   • S2 et S1 sont étiquetés ∀(Z U Y) car, depuis ces états, tous les chemins traversent des états où Z est vrai jusqu'à atteindre S3 (Y).
3. Traitement de l'implication (X → ∀(Z U Y)) : Cette formule est équivalente à ¬X ∨ ∀(Z U Y). L'algorithme étiquette les états où X est faux (comme S0 et S3) OU l'étiquette ∀(Z U Y) est présente (S1, S2, S3). Tous les états {S0, S1, S2, S3} reçoivent donc cette étiquette.
4. Traitement de ∀(...) : Puisque la sous-formule est vraie dans tous les états du modèle, la formule globale est vérifiée dès l'état initial.

Question 5 - Preuve d'équivalence ¬(p → Oq) ⇔ ◊(p ∧ O¬q)

Il s'agit de démontrer l'équivalence en appliquant les lois de la logique temporelle. Note : O désigne l'opérateur "Next" (Suivant), et ◊ l'opérateur "Eventuellement" (F).

• Formule initiale : ¬(p → Oq)
• Étape 1 : Par la dualité des opérateurs temporels ( ¬φ ⇔ ◊¬φ ), nous obtenons : = ◊¬(p → Oq)
• Étape 2 : En appliquant la définition de l'implication matérielle ( p → q ⇔ ¬p ∨ q ) : = ◊¬(¬p ∨ Oq)
• Étape 3 : En appliquant la loi de De Morgan sur la négation : = ◊(¬(¬p) ∧ ¬Oq) = ◊(p ∧ ¬Oq)
• Étape 4 : Par la propriété de l'opérateur "Next", nier que la propriété soit vraie au prochain état est équivalent à affirmer que sa négation sera vraie au prochain état ( ¬Oq ⇔ O¬q ) : = ◊(p ∧ O¬q)

L'équivalence est donc formellement démontrée.

Question 6 - Vérification de l'équivalence p ⇔ p ∧ Op

Nous devons vérifier cette équivalence par preuve sémantique sur une trace (chemin d'exécution) nommée σ, où σ0 représente l'état courant et σi le i-ème état du chemin.

Soit σ un chemin. σ |= p ⇔ ∀ i ≥ 0, (σi |= p) (Par définition de l'opérateur Toujours ) ⇔ (σ0 |= p) ∧ (∀ i ≥ 1, (σi |= p)) (On isole l'instant présent (i=0) du futur (i≥1)) ⇔ (σ0 |= p) ∧ (σ1 |= p) (Dire que p est vrai pour tout i≥1 équivaut à dire que p est vrai à partir de l'état 1) ⇔ (σ0 |= p) ∧ (σ0 |= Op) (Dire que p est vrai à l'état 1 équivaut à dire que le "Next" (O) de p est vrai à l'état 0) ⇔ σ0 |= (p ∧ Op) ⇔ p ∧ Op

La propriété récursive (déploiement de l'opérateur ) est donc prouvée vraie.

Question 7 - Propriété d’atteignabilité dans un programme

Le fragment de programme est une boucle "Répéter ... Jusqu’à" qui demande un entier et s'arrête lorsque cet entier est compris entre 10 et 100, pour ensuite l'afficher.

Début
Répéter
  Ecrire(‘donner un entier entre 10 et 100’) ;
  Lire(n) ;
Jusqu’à n dans [10..100] ;
Affichage (n) ;
Fin

• Expression de la propriété d'atteignabilité : Nous voulons exprimer qu'il existe un chemin d'exécution capable d'atteindre l'instruction. Formule : ∃◊(Affichage(n)) (ou EF(Affichage(n)) en syntaxe CTL standard) On peut également l'écrire sous forme d'implication depuis le début : Début → ∃◊(Affichage(n)).

• Vérification de cette propriété : La propriété est vraie. Il suffit de trouver une trace qui satisfait la condition de sortie de boucle. Si, à la première itération, l'utilisateur saisit la valeur 15 (qui est bien dans l'intervalle [10..100]), la condition n dans [10..100] est évaluée à Vrai, le programme sort de la boucle et exécute Affichage(n). Puisqu'il existe au moins une telle trace d'exécution, la propriété ∃◊(Affichage(n)) est validée.

Exercice Producteur/consommateur Partie II

Question 1 - La vérification de modèle

(Ce point constitue le titre de la section dans la source).

Question 2 - Types des propriétés P1 et P2

• P1 : Vivacité (Liveness) Explication : Une propriété de vivacité affirme que "quelque chose de bien finira par arriver". Ici, la propriété garantit que toute demande du producteur ou du consommateur finira par être satisfaite (une action future est garantie).
• P2 : Sûreté (Safety) Explication : Une propriété de sûreté affirme que "quelque chose de mal n'arrivera jamais". Ici, on s'assure que le producteur et le consommateur ne peuvent jamais se retrouver en même temps dans la section critique (exclusion mutuelle).

Question 3 - Expression des propriétés en logique PLTL

• Propriété P1 (Vivacité) en PLTL : Formule : G(demandeP → F Prod) ∧ G(demandeC → F Cons) Explication : "Toujours (G), si une demande producteur est faite, alors dans le futur (F) une production aura lieu, ET Toujours, si une demande consommateur est faite, alors dans le futur une consommation aura lieu". Note pour le CTL : La source fournit également l'équivalent en logique arborescente CTL : AG(demandeP → AF Prod) ∧ AG(demandeC → AF Cons).

• Propriété P2 (Sûreté) en PLTL : Formule : G¬(prod ∧ cons) Explication : "Toujours (G), il est faux que (¬) le producteur et le consommateur soient actifs en même temps". Note pour le CTL : Son équivalent en CTL est AG¬(prod ∧ cons).

Méthode

Face à une épreuve de Logique Temporelle formelle, la rigueur syntaxique et la compréhension des opérateurs sont indispensables :

1. Distinguer la logique linéaire (LTL/PLTL) de la logique arborescente (CTL) : En LTL, on raisonne sur un seul chemin d'exécution, on utilise donc uniquement des opérateurs temporels (G, F, X/O, U). En CTL, le système est vu comme un arbre de futurs possibles ; chaque opérateur temporel doit obligatoirement être précédé d'un quantificateur de chemin (A pour Tous les chemins, E/∃ pour Il existe un chemin).
2. Savoir déployer les formules : Les équivalences telles que G p ⇔ p ∧ X(G p) ou F p ⇔ p ∨ X(F p) (et leurs preuves associées via sémantique de traces) reviennent presque systématiquement. Elles sont la base du "model checking" et permettent de prouver récursivement le fonctionnement d'un automate.
3. Décoder les artefacts typographiques : Sur des annales numérisées, il est fréquent que les polices mathématiques aient sauté (ici,  remplaçant □, X remplacé par O pour l'opérateur Next, ou des quantificateurs étrangement placés). Appuyez-vous toujours sur le contexte (vivacité, sûreté) pour déduire l'opérateur correct. Ne restez pas bloqué sur un symbole inconnu.