M2 Info Paris 7
Modélisation - Partiel 2018-2019
Éléments de corrections (non officiels)


== Exercice 3 ==
=== Exercice 3 - Partie 1 ===

Remarque : Comme le précise le sujet, une formule LTL est "vraie pour S" si et seulement si elle est vraie pour TOUTES les exécutions de S.

1) aUb
Faux
Traduction de la formule LTL : Dans toutes les exécutions, on va avoir un jour B, et jusque là on a toujours des A
Justification : Faux car il existe une exécution dans laquelle on n'a jamais B : q0-q1-q1-q1-... 

2) ¬(aUb)
Faux
Traduction de la formule LTL : Dans aucune exécution, on ne va avoir un jour B, et jusque là toujours des A
Justification : Faux car la plupart des exécutions (toutes hormis celle citée à la question précédente) respectent bien la condition aUb

3) GFb
Faux 
Traduction de la formule LTL : Dans toutes les exécutions, il y a une infinité de B
Justification : (idem point 1) Faux car il existe une exécution dans laquelle on n'a jamais B : q0-q1-q1-q1-... 

4) G(a∨b)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, on a toujours A ou B
Justification : Trivialement vrai, car tous les états comportent un A ou un B

5) (GFb) ⇒ (GFc)
Faux
Traduction de la formule LTL : Dans toutes les exécutions, si on a une infinité de B, alors on a aussi une infinité de C
Justification : On peut trouver des exécutions avec une infinité de B mais par une infinité de C, par exemple la boucle : q0-q1-q3- q0-q1-q3- q0-q1-q3- ...

6) (FG¬a) ⇒ (aUb)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, si un jour on ne trouve plus de A, alors... (inutile d'aller plus loin pour savoir que c'est vrai)
Justification :
	La première partie de l'implication est toujours fausse : il n'existe aucune exécution dans laquelle on ne trouve plus de A passé un certain point
	La formule est donc toujours vraie, car quel que soit X : (Faux⇒X) = Vrai

9) (Fc) ⇒ (aUb)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, si on a un jour C, alors on a un jour B, et jusque là toujours A.
Justification :
	La seconde partie de l'implication est toujours Vraie, sauf pour l'exécution q0-q1-q1-q1... à l'infini (cf. question 1)
	La première partie de l'implication est fausse pour l'exécution q0-q1-q1-q1... à l'infini
	Donc il n'existe aucune exécution qui puisse faire "Vrai ⇒ Faux" (seul moyen de contre-dire une implication)
	Donc l'implication est Vraie pour toutes les exécutions

8) (GFc)⇒(GFb)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, si on a une infinité de C, alors on a aussi une infinité de B
Justification :
	Pour avoir une infinité de C, il faut passer une infinité de fois en q2
	Chaque fois qu'on passe en q2, on passe forcément en q3 le lendemain, ce qui donne un B
	Donc si on a une infinité de C, on a aussi une infinité de B


=== Exercice 3 - Partie 2 ===

Remarque :
Pour les cas pas équivalents, un contre-exemple suffit.
Pour les cas équivalents, une démonstration formelle basée sur les définitions des symboles (données dans l'énoncé) était peut-être apprécié, mais on se contentera ici de quelques phrases de justification.

1) FFa ≡? Fa
Équivalentes
Les deux formules signifient qu'on aura un jour A

2) F(a∧b) ≡? Fa ∧ Fb
Pas équivalentes
Si on a A et B deux jours différents, la première formule est fausse et la seconde est vraie
Remarque : La première formule implique la seconde

3) F(a ∧ Xb) ≡? F(a ∧ Fb)
Pas équivalentes
Si on a un A puis un B deux jours plus tard, la première formule est fausse et la seconde est vraie
Remarque : La première formule implique la seconde

4) GF(a∨b) ≡? GFa ∨ GFb
Équivalentes
Les deux formules signifient qu'on trouve une infinité de jours avec la lettre A ou la lettre B.
S'il y a une infinité de fois la lettre A ou lettre B, alors il y en a au moins une des 2 présente une infinité de fois.
Et inversement, s'il y a une infinité de fois la lettre A, ou une infinité de fois la lettre B, alors on trouve une infinité de fois un A ou un B.
Remarque 1 :
	Le mot "ou" est évidemment à prendre ici dans le sens logique et inclusif, c'est-à-dire que les propositions 2 peuvent être vraies, alors que dans le langage courant il est plus souvent utilisé au sens exclusif ("XOR"), c'est-à-dire que seule l'une des 2 proposition peut être vraie.
Remarque 2 :
	Si on dit la phrase "Il y a au moins 10 fois A ou B", ça n'est pas équivalent à "Il y a au moins 10 fois A, ou il y a au moins 10 fois B", car il peut y en avoir par exemple 5 de chaque (ce qui rend la première phrase vraie et la seconde fausse).
	Mais si on dit "Il y a une infinité de fois A ou B", c'est bien équivalent à "Il y a une infinité fois A, ou il y a une infinité de fois B" car une "demi-infinité" fait toujours une infinité. Par exemple : Il y a une infinité de nombres entiers, mais aussi une infinité de nombres pairs.