**Exercice 1 (Principal 2015)**
1. Répondre aux questions suivantes :
– Fp est-il vrai si p est vrai tout de suite dans l’état courant ?
– Gp est-il vrai si p est faux dans l’état courant et vrai partout ailleurs ?
– pUq est-il vrai si p est faux et q est vrai dans l’état courant ?
– pUq est-il vrai si q est toujours faux, et p est toujours vrai ?
1. Exprimer les propriétés suivantes dans une exécution arborescente:
P2. Quelque soit l’état, on finit par aller à un état où p est vrai.
P3. Quelque soit l’état, on peut aller à un état où p est vrai.
1. Donner un modèle kripke qui satisfait la propriété P2. 2. Donner un modèle kripke qui satisfait la propriété P3.
**UNE Correction Possible de l’Exercice 1 :**
1)
- oui
- non
-oui
-non
2)
P2) AGAFp
p
Publicité
p
p
P3) AGEFp
p
**Exercice2 (Principal 2014)**
1. Donner en logique PLTL une formule temporelle décrivant la propriété qui indique qu’à 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. 2. Formaliser la même propriété dans la logique temporelle arborescente CTL 3. Construire un automate (structure Kripke) où la formule donnée en (2) est satisfaite. On peut considérer que X : « timeout », Z : « avertissement » et Y : « rejet ou réponse » 4. Vérifier cette formule en montrant la trace d’exécution de l’algorithme de model checking de CTL. 5. Montrer que la négation de la formule (p →Oq) est équivalente à la formule ◊(p ∧ O¬q) 6. Vérifier si l’équivalence p ⇔ p ∧ Op est vérifiée (par preuve si vrai et par un contre exemple dans le cas contraire) 7. Exprimer la propriété d’atteignabilité de l’instruction d’affichage dans le fragment du programme suivant (c'est-à-dire qu’il existe un chemin d’exécution où l’affichage est réalisé)
Début
Répéter
Ecrire(‘donner un entier entre 10 et 100’) ;
Lire(n) ;
Jusqu’à n dans [10..100] ;
Affichage (n) ;
Fin
Vérifier cette propriété d’atteignabilité.
**UNE Correction Possible de l’Exercice 2 :**
(X → (Z U Y)
∀(X → ∀(Z U Y)
1. Construire un automate (structure Kripke) où la formule donnée en (2) est satisfaite. On peut considérer que X : « timeout », Z : « avertissement » et Y : « rejet ou réponse »
réponse
Publicité
Avert
Timeout, Avert
rejet
Principalement c ca mais on peut admettre avec réponse Avert ou timeout
L’eesentiel c que toute exécution qui arrive à timeout arrive aussi à Avert et restera vraie jusqu’à avoir réponse ou rejet
1. Vérifier cette formule en montrant la trace d’exécution de l’algorithme de model checking de CTL. 2. Montrer que la négation de la formule (p →Oq) est équivalente à la formule ◊(p ∧ O¬q)
¬(p →Oq) = ¬(¬p∨Oq) = ◊¬(¬p∨Oq) =◊(p∧¬Oq) = ◊(p∧O¬q)
1. Vérifier si l’équivalence p ⇔ p ∧ Op est vérifiée (par preuve si vrai et par un contre exemple dans le cas contraire) :
σ |= p ⇔ ∀ i (i≥0 ∧ i ≤ |σ|) (σi |= p)
⇔ σ0 |= p ∧ ∀ i (i≥1 ∧ i ≤ |σ|) (σi |= p )
⇔ σ0 |= p ∧ σ1 |= p
⇔ σ0 |= p ∧ σ0 |= Op
⇔ σ0 |= (p ∧ Op)
⇔ p ∧ Op
1. Exprimer la propriété d’atteignabilité de l’instruction d’affichage dans le fragment du programme suivant (c'est-à-dire qu’il existe un chemin d’exécution où l’affichage est réalisé):
Début
Répéter
Ecrire(‘donner un entier entre 10 et 100’) ;
Lire(n) ;
Publicité
Jusqu’à n dans [10..100] ;
Affichage (n) ;
Fin
∃◊(Affichage(n))
ou
Début →∃◊(Affichage(n))
……
**Exercice Producteur/consommateur Partie II :**
1. **La vérification de modèle (1.5pts)** 2. Quels sont les types des propriétés P1 et P2. (0.5pt)
P1 : vivacité
P2 : Sûreté
1. Exprimer, en utilisant la logique temporelle linéaire propositionnelle PLTL, les propriétés P1 et P2. (1pt)
P1: G(demandeP → F Prod) ∧ G(demandeC → F Cons)
P2: G¬ (prod ∧ cons)
P1: AG(demandeP → AF Prod) ∧ AG(demandeC → AF Cons)
P2: AG¬ (prod ∧ cons)