Correction TD de Model Checking
Logiques temporelles
Exercice 1. La vivacit e est-elle de la s uret e ? Justiez.
Correction. La vivacit e est di erente de la s uret e car pour une ex ecution qui ne satisfait pas par exemple Fp, on ne peut
d eduire quelle est fausse en regardant juste un pr exe pass e.
Exercice 2. Quelques petits exercices sur les connecteurs temporels :
Fp est-il vrai si p vrai tout de suite dans l etat courant ?
Gp est-il vrai si p faux dans l etat courant et vrai partout ailleurs ?
pUq est-il vrai si p faux et q vrai dans l etat courant ?
pUq est-il vrai si q est toujours faux, et p toujours vrai ?
Correction. oui, non, oui, non
Exercice 3. Dessinez des d epliages sur lesquels vous illustrerez les propri et es EX, AX, EU, AU.
Correction. Attention pour EpUq et ApUq `a ce que p soit vrai au d ebut (si q faux).
Exercice 4. Exprimer les propri et es suivantes :
1. Tous les etats satisfont p.
2. On peut atteindre p par un chemin o`u q est toujours vrai.
3. Quelquesoit l etat, on nit par revenir `a l etat initial init.
4. Quelquesoit l etat, on peut revenir `a l etat initial init.
5. Absence de deadlock (partiel).
Correction.
1. AGp (classique de linvariance)
2. E(Fp ' Gq), ou bien E(qUp) selon le sens que lon donne `a la phrase (voyez-vous la di erence ?)
3. AGAFp (dautres traductions comme AFp se basent sur le fait que init est initial, mais seraient fausses pour
dautres propri et es. D esol e lexemple nest pas tr`es bon)
4. AGEFp
Publicité
5. AGEXtrue (vu la s emantique, ne peut etre faux que si il existe un etat sans successeur ; cest plus une astuce `a
avoir vue que quelquechose de vraiment utile).
1
Exercice 5. On va voir que certains connecteurs sont redondants.
1. Exprimer Gp avec les connecteurs , F et p.
2. Exprimer Fp gr ace au connecteur U.
3. Peut-on exprimer X en fonction des autres connecteurs ?
4. Peut-on exprimer U en fonction des autres connecteurs ?
Correction.
1. Gp a F p
2. Fp a trueUp
3. non. Dicile `a d emontrer, mais intuitivement X est le seul op erateur qui impose fortement quand doit avoir lieu
lobservation (au prochain coup, ni avant ni apr`es). Les autres connecteurs sont plus l aches.
4. non. Dicile `a d emontrer, mais intuitivement U est le seul op erateur qui combine deux sous-formules.
Exercice 6 (Autres connecteurs.). On va d enir quelques connecteurs additionels utiles.
1. D enir la relation |= pour les connecteurs additionnels suivants :
pWq (weak until) : signie que p est vrai jusqua ce que q soit vrai, mais q nest pas forc ement vrai a
un moment. Dans ce cas, p reste vrai tout le long du chemin.
Fp (inniment souvent) : p est inniment vrai au long de lex ecution.
Gp (presque toujours) : `a partir dun moment donn e, p est toujours vrai.
p Udkq (bounded until) : p vrai jusqu`a ce que q soit vrai, et q vrai dans au plus k observations.
pRq (release) : q est vraie jusqua (et inclus) le premier etat ou p est vraie, sachant que p nest pas
forc ement vraie un jour.
2. On va maintenant faire le lien entre ces connecteurs et les anciens.
Exprimer F, G, W, Udk par des connecteurs de basiques de LTL.
Publicité
Exprimer U dans LTL-U+W.
Correction.
1.
|= 1W 2 i (il existe k e 0 tel que k |= 2 et pour tout 0 d j < k j |= 1) ou pour tout k k |= 1
|= F i pour tout k, il existe j e k tel que j |=
|= G i il existe k tel que pour tout j e k on a j |=
|= 1Udk 2 i il existe 0 d i d k tel que i |= 2 et pour tout 0 d j < i j |= 1
2.
pWq a (pUq) ( Gp ; Fp a GFp ; Gp a FGp ;
Deux traductions pour Udk :
pUdkq a pUq ' (q ( Xq ( . . . ( Xkq)
ou
pUdkq a (q ( (p ' Xq) ( . . . ( (p ' Xp ' . . . ' Xk1p ' Xkq))
pUq a (pWq) ' Fq, et F sobtient `a partir de G, car Gp a pWf alse
Exercice 7. Parmi les op erateurs suivants, lesquels correspondent plut ot `a des propri et es de s uret e ?
X, F, G, U, W, Udk, F, G.
Correction. R e echir en termes de contre-exemple nis ou non. S uret e (ou sous-classes de s uret e) : X, G, W, Udk
Exercice 8. Exprimer en langage naturel les propri et es suivantes.
AG(emission Freception)
2
AFok G(emission Freception)
Correction. 1. Pour tout chemin, une emission (de message) est toujours suivi par une r eception (de message)
2. pour tout chemin, si on a inniment souvent ok, alors une emission (de message) est toujours suivi par une
r eception (de message).
Exercice 9. Exprimer toutes les propri et es de la section 3.1 en tenant compte des quanticateurs de chemin.
Publicité
Correction.
Exercice 10 (CTL).
1. Montrer que (, , X, U et E susent `a exprimer les autres connecteurs.
2. Montrez que si on ajoute R, on peut restreindre aux propositions atomiques.
Correction.
1. On revient `a lexo 11 pour exprimer F et G, bien entendu 1 ' 2 a ( 1 ( 2), et on v erie que A a E
Exercice 11 (CTL). Montrer que p, (, , EX, EG et EU susent `a exprimer les autres connecteurs.
Montrer ensuite que p, ', , EX, AU et EU susent aussi.
Correction. Le second est plus facile.
1. On traduit les op erateurs manquants comme suit :
AX a EX
AF a EG
EF a EtrueU
AG a EF
A 1U 2 a ((E( 1 ' 2)U( 1 ' 2)) ( (EG 2))
2. On traduit les op erateurs manquants comme suit :
AX a EX
AF a AtrueU
EF a EtrueU
AG a EF
EG a AF
3