Correction TD de Model Checking

Exercice 1 - La vivacité est-elle de la sûreté ?

La vivacité (liveness) est fondamentalement différente de la sûreté (safety).

Une propriété de sûreté stipule que "rien de mauvais n'arrive". Si elle est violée, on peut toujours le prouver en observant un préfixe fini de l'exécution (une trace finie où le mauvais événement s'est produit).

Une propriété de vivacité, en revanche, stipule que "quelque chose de bien finira par arriver" (par exemple Fp, "p sera éventuellement vrai"). Si l'on observe une exécution partielle (un préfixe passé) qui ne satisfait pas p, on ne peut pas en déduire que la propriété est fausse pour toute l'exécution, car p pourrait très bien devenir vrai dans le futur. La vivacité ne peut donc pas être réfutée par un simple préfixe fini.

Exercice 2 - Évaluation de connecteurs temporels

• Fp est-il vrai si p vrai tout de suite dans l'état courant ? Oui. L'opérateur F (Future / Eventually) inclut le présent. Si p est vrai à l'étape actuelle, Fp est immédiatement satisfait.
• Gp est-il vrai si p faux dans l'état courant et vrai partout ailleurs ? Non. L'opérateur G (Globally) exige que la propriété soit vraie à chaque instant de l'exécution, y compris l'état initial (courant).
• pUq est-il vrai si p faux et q vrai dans l'état courant ? Oui. L'opérateur U (Until) demande que p soit vrai jusqu'à ce que q le devienne. Si q est vrai dès le départ, il n'y a aucune exigence sur p.
• pUq est-il vrai si q est toujours faux, et p toujours vrai ? Non. La sémantique standard de U (Until fort) exige que l'événement q finisse obligatoirement par se produire. Si q n'arrive jamais, la formule est fausse.

Exercice 3 - Dépliages et propriétés EX, AX, EU, AU

Pour illustrer ces propriétés, imaginez un arbre de calcul (dépliage) dont la racine est l'état courant s0.

• EX p : À partir de la racine s0, il existe au moins une branche (un chemin) menant à un état successeur immédiat s1 où p est vrai.
• AX p : À partir de la racine s0, pour toutes les branches possibles, l'état successeur immédiat satisfait p.
• E(p U q) : Il existe au moins un chemin partant de s0 sur lequel q finit par être vrai dans un état futur, et pour tous les états précédents sur ce chemin, p est vrai. (Attention : si q n'est pas vrai immédiatement à la racine, p doit impérativement y être vrai).
• A(p U q) : Sur absolument tous les chemins partant de s0, on finit par rencontrer un état où q est vrai, et sur chaque chemin, p reste vrai à chaque étape jusqu'à ce que q soit rencontré.

Exercice 4 - Expression de propriétés

Question 1 - Tous les états satisfont p

AG p (Invariance classique : sur tous les chemins, globalement p).

Question 2 - Atteindre p par un chemin où q est toujours vrai

E(q U p) ou bien E(Fp ∧ Gq) selon l'interprétation exacte. La différence est subtile :

• E(q U p) signifie qu'il existe un chemin où q est vrai jusqu'à ce qu'on atteigne p. Une fois p atteint, q n'est plus obligé d'être vrai.
• E(Fp ∧ Gq) exige qu'il existe un chemin où p est atteint à un moment, mais où q doit rester vrai globalement, même après avoir atteint p, et ce pour toujours.

Question 3 - Quel que soit l'état, on finit par revenir à l'état initial

AG AF init (Le corrigé source mentionne AG AF p mais note que l'utilisation d'une proposition spécifique "init" est plus appropriée ici pour marquer l'état).

Question 4 - Quel que soit l'état, on peut revenir à l'état initial

AG EF init (Partout, il existe un chemin possible ramenant à init).

Question 5 - Absence de deadlock (partiel)

AG EX true (La sémantique de EX true signifie qu'il y a au moins un état suivant valide. L'imposer partout avec AG garantit qu'aucun état de l'automate n'est un puits sans successeur).

Exercice 6 - Connecteurs additionnels (et Exercice 5)

(Note : La correction fournie regroupe implicitement la fin de l'Exercice 5 dans sa propre logique, bien que les titres du document source puissent paraître mélangés. L'Exercice 5 démontrait la redondance : Gp ≡ ¬F¬p, Fp ≡ true U p, et l'impossibilité d'exprimer X et U avec les autres car X impose une observation stricte au pas suivant et U est le seul à combiner deux sous-formules).

Question 1 - Définition de la relation (|=) pour connecteurs additionnels

Soit σ une exécution, et σ_i le i-ème état de cette exécution.

• p W q (Weak Until) : σ |= ϕ1 W ϕ2 ssi (il existe k ≥ 0 tel que σ_k |= ϕ2 et pour tout 0 ≤ j < k, σ_j |= ϕ1) OU (pour tout k, σ_k |= ϕ1).
• F∞ p (Infiniment souvent) : σ |= F∞ϕ ssi pour tout k, il existe j ≥ k tel que σ_j |= ϕ.
• G∞ p (Presque toujours) : σ |= G∞ϕ ssi il existe k tel que pour tout j ≥ k on a σ_j |= ϕ.
• p U≤k q (Bounded Until) : σ |= ϕ1 U≤k ϕ2 ssi il existe 0 ≤ i ≤ k tel que σ_i |= ϕ2 et pour tout 0 ≤ j < i, σ_j |= ϕ1.
• p R q (Release) : La source omet la définition mathématique dans sa correction. Formellement, σ |= ϕ1 R ϕ2 ssi pour tout k ≥ 0, si pour tout 0 ≤ i < k on a σ_i ⊭ ϕ1, alors σ_k |= ϕ2. (q doit être vrai jusqu'à ce que p le libère, inclusivement).

Question 2 - Liens entre les connecteurs

• Expression des nouveaux connecteurs en LTL basique :

  • p W q ≡ (p U q) ∨ Gp
  • F∞ p ≡ GF p
  • G∞ p ≡ FG p
  • p U≤k q peut se traduire de deux manières en déroulant l'opérateur : p U≤k q ≡ p U q ∧ (q ∨ Xq ∨ ... ∨ X^k q) ou bien p U≤k q ≡ (q ∨ (p ∧ Xq) ∨ ... ∨ (p ∧ Xp ∧ ... ∧ X^{k-1}p ∧ X^k q))

• Expression de U dans LTL avec U remplacé par W :

  • p U q ≡ (p W q) ∧ Fq
  • Sachant que F s'obtient à partir de G car Gp ≡ p W false (p reste vrai indéfiniment sans jamais que false ne devienne vrai), d'où Fp ≡ ¬G¬p.

Exercice 7 - Propriétés de sûreté

Parmi les opérateurs donnés (X, F, G, U, W, U≤k, F∞, G∞), ceux qui correspondent à des propriétés de sûreté (ou sous-classes) sont : X, G, W, U≤k. La justification repose sur le fait que la violation de ces propriétés peut toujours être prouvée à l'aide d'un contre-exemple fini (une exécution partielle qui contredit la règle).

Exercice 8 - Propriétés en langage naturel

• AG(emission → Freception) Pour tout chemin, une émission (de message) est toujours suivie, à un moment ou un autre, par une réception (de message).
• AF∞ok → G(emission → Freception) Pour tout chemin, si on a infiniment souvent "ok", alors une émission de message est toujours suivie par une réception de message.

Exercice 9 - Propriétés de la section 3.1

(Note : Le document source ne contient ni les énoncés de la section 3.1, ni leur correction textuelle. Cette question est impossible à résoudre sans le texte d'origine complet de la section 3.1).

Exercice 10 - CTL*

Question 1 - ∨, ¬, X, U et E suffisent à exprimer les autres

• ∧ s'obtient par De Morgan : ϕ1 ∧ ϕ2 ≡ ¬(¬ϕ1 ∨ ¬ϕ2)
• A s'obtient par dualité avec E : Aϕ ≡ ¬E¬ϕ
• F et G s'obtiennent via U : Fϕ ≡ true U ϕ, et Gϕ ≡ ¬F¬ϕ.

Question 2 - Ajout de R et restriction de ¬ aux propositions atomiques

(Note : La correction source est tronquée pour cette question. Le principe théorique sous-jacent est que R (Release) est le dual de U (Until). Grâce aux équivalences ¬(p U q) ≡ ¬p R ¬q et ¬(p R q) ≡ ¬p U ¬q, on peut pousser toutes les négations vers le bas de l'arbre syntaxique jusqu'aux propositions atomiques, éliminant ainsi le besoin de ¬ devant des formules complexes).

Exercice 11 - CTL

Question 1 - Exprimer le reste avec p, ∨, ¬, EX, EG, EU

• AXϕ ≡ ¬EX¬ϕ
• AFϕ ≡ ¬EG¬ϕ
• EFϕ ≡ E(true U ϕ)
• AGϕ ≡ ¬EF¬ϕ
• A(ϕ1 U ϕ2) ≡ ¬((E(ϕ1 ∧ ¬ϕ2) U (¬ϕ1 ∧ ¬ϕ2)) ∨ (EG¬ϕ2)) (Cette formule combine la recherche d'un chemin où l'on échoue à vérifier ϕ1 avant d'atteindre ϕ2, ou un chemin où ϕ2 n'arrive jamais).

Question 2 - Exprimer le reste avec p, ∧, ¬, EX, AU, EU

Cette traduction est plus directe :

• AXϕ ≡ ¬EX¬ϕ
• AFϕ ≡ A(true U ϕ)
• EFϕ ≡ E(true U ϕ)
• AGϕ ≡ ¬EF¬ϕ
• EGϕ ≡ ¬AF¬ϕ

Méthode

Face à une épreuve de Model Checking portant sur les logiques temporelles (LTL, CTL, CTL*) :

1. Distinguez les quantificateurs : Séparez rigoureusement ce qui relève de la structure de l'arbre (les quantificateurs de chemins : A pour "All", E pour "Exists") de ce qui relève du temps sur un chemin unique (G pour globalement, F pour le futur, X pour le pas suivant, U pour Until).
2. Maîtrisez les dualités : Apprenez par cœur les relations de dualité temporelles et existentielles. Vous devez savoir instantanément que ¬AX p ≡ EX ¬p, ou que ¬G p ≡ F ¬p. C'est la clé de voûte des exercices de redondance syntaxique.
3. Tracez des contre-exemples (Kripke) : Lorsque l'on vous demande si une formule implique une autre ou d'évaluer une sémantique (comme pour Fp vs Gp), dessinez rapidement une petite structure d'états (Automate / Structure de Kripke) avec 2 ou 3 nœuds et une boucle. Vérifiez si vous pouvez forcer la première formule à être vraie tout en rendant la seconde fausse.
4. Attention aux conditions initiales de 'Until' : Souvenez-vous que p U q nécessite toujours que p soit vrai à l'état courant si q n'y est pas encore. Une erreur classique est de vérifier p seulement à partir du pas suivant.