M2 Info Paris 7
Modélisation - Partiel 2017-2018
Eléments de corrections (non officiels)



== Exercice 3 ==

1) aUb
Vrai
On va avoir un jour B : Vrai (le 2ème jour, en q1)
Et jusqu'à ce jour, on a toujours A : Vrai (le 1er jour, on a A en q0)

2) X(aUb)
Vrai
A partir de demain (donc on est forcément en q1) on va avoir un jour B : Vrai (on est dans un état avec B)
(inutile donc de vérifier si on a des A avant, puisque B est vrai tout de suite)

3) G(c ⇒ (aUb))
Vrai
A chaque fois qu'on a C (donc quand on est en q2 ou en q3)
Alors B va devenir vrai un jour (vrai pour q2 qui aura forcément B le lendemain, et vrai pour q3 qui a déjà B)
Et jusqu'à ce jour, on a toujours A (vrai pour q2, qui a A le premier jour et trivialement vrai pour q3 qui a déjà B)

4) GFa
Faux
On a une infinité de A : ça n'est pas vrai pour toutes les exécutions
Les exécutions qui vont un jour boucler indéfiniment en q3 ne vérifient pas cette formule

5) FGc ⇒ G(a⇒Xb)
Vrai
Si un jour on a toujours C (donc pour toutes les éxecutions qui vont un jour boucler indéfiniment dans les états q2 et q3)
Alors chaque fois qu'on a A (donc quand on est en q0 ou en q2)
On aura B le lendemain : Vrai (à partir de q0 ou de q2, on a forcément B le lendemain)

6) FGc ⇒ G(b⇒Xa)
Faux
Si un jour on a toujours C (donc pour toutes les éxecutions qui vont un jour boucler indéfiniment dans les états q2 et q3)
Alors chaque fois qu'on a B (donc quand on est en q1 ou en q3)
On aura A le lendemain : Faux (à partir de q3 on peut rester en q3, on a donc pas forcément A le lendemain)

7) GFb
Vrai
Il y a une infinité de B : Vrai (il n'y a aucun endroit où on pourrait boucler sans jamais avoir B)



== Exercice 4 ==

1) G¬a
(ou la formule équivalente : ¬Fa)

2) Fa

3) GFa

4) ¬a U (a ∧ XG¬a)
Il y n'y aura pas de A, jusqu'au jour où on trouve un A, et à partir du lendemain on ne trouve plus jamais de A

5) ¬a U (a ∧ X[¬a U (a ∧ XG¬a)])
Il y n'y aura pas de A, jusqu'au jour où on trouve un A, et à partir du lendemain [on trouvera un seul A]
(on réutilise la question précédente pour la partie entre crochets dans la phrase et dans la formule)

6) [(a∧¬b) ∨ (¬a∧b)] ∧ G[(a ⇒ X(¬a∧b)) ∧ (b ⇒ X(¬b∧a))]
Le premier jour, A ou B est vrai (mais pas les deux)
Chaque fois que A est vrai, le lendemain A est faux et B est vrai.
Chaque fois que B est vrai, le lendemain B est faux et A est vrai.

7) (GFa) ⇒ (Gb)



== Exercice 5 ==

1) F(a∧b) --- (Fa)∧(Fb) 
Pas équivalent
Exemple : si A et B arrivent 2 jours différents, alors la première formule est fausse mais la seconde est vraie.
(par contre la première formule implique la seconde)

2) G(a∧b) --- (Ga)∧(Gb)
Equivalent
première formule = A et B toujours vrai
deuxième formule = A toujours vrai et B toujours vrai
Les 2 phrases sont bien équivalentes

3) aUb --- Ga ∧ Fb
Pas équivalent
Exemple : Si on a des A jusqu'au premier B et plus de A ensuite, alors la première formule est vraie mais la seconde est fausse.
(par contre la seconde formule implique la première)

4) Fa ∧ Fb --- F(a ∧ Fb) ∨ F(b ∧ Fa) 
Equivalent
première formule = Un jour A et un jour B
deuxième formule = Un jour A puis B plus tard (ou en même temps) ou un jour B puis A plus tard (ou en même temps)
Les 2 phrases sont bien équivalentes