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



== Exercice 3 ==

Remarque :
	L'exercice 3 de ce partiel est très proche de l'exercice 3 du partiel 2018-2019.
	Le STE est presque inchangé (ajout d'une boucle sur l'état q3) et la plupart des questions sont reprises.
	Les questions nouvelles ou dont la réponse change par rapport au partiel précédent sont marquées par une étoile (*).

=== Exercice 3 - Partie 1 ===

Remarque : Comme le précise le sujet, une formule LTL est "vraie pour S" si elle 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*) aWb
Vrai
Remarque : Comme le précise le sujet, aWb est une abréviation pour "aUb ∨ Ga"
Traduction de la formule LTL : Dans toutes les exécutions, soit on va avoir un jour B et jusque là toujours des A, soit toujours A
Justification : Vrai car aUb est vrai dans toutes les exécution sauf celle données à la question 1, dans laquelle Ga est vrai
Autre justification possible :
	Tous les états portent un A ou un B.
	Donc, de façon triviale et sans même regarder les transitions :
		soit on va passer un jour par un B et on a alors "aUb",
		soit non et on a alors "Ga".

3) ¬(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 1) respectent bien la condition aUb

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

5) 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

6) (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 : Faux car 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- ...

7*) (FGa) ∨ (FGb)
Faux
Traduction de la formule LTL :
	Dans toutes les exécutions,
	soit on aura A toujours vrai à partir d'un certain jour,
	soit on aura B toujours vrai à partir d'un certain jour.
Justification :
	Faux car il existe plein d'exécution on où n'aura jamais ni toujours A ni toujours B.
	Par exemple (comme dans la question 6) la boucle : q0-q1-q3- q0-q1-q3- q0-q1-q3- ...

8*) (FG¬a) ⇒ (aUb)
Vrai
Remarque :
	Cette formule était déjà présente dans le partiel précédent et elle reste vraie.
	Mais la justification est différente en raison de la boucle ajoutée sur l'état q3.
Traduction de la formule LTL : Dans toutes les exécutions, si un jour on ne trouve plus de A, alors on a toujours eu des A jusqu'à avoir un B
Justification :
	La première partie de l'implication est toujours Fausse, sauf pour les exécutions qui terminent en q3-q3-q3... à l'infini
	La seconde partie de l'implication est toujours Vraie, sauf pour l'exécution q0-q1-q1-q1... à l'infini (cf. question 1)
	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

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

10) (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ée,
	mais on se contentera ici de quelques phrases de justification.

1) F(a∧b) ≡? Fa ∧ Fb
Pas équivalentes
Contre-exemple : 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

2*) G(a∧b) ≡? Ga ∧ Gb
Équivalentes
Justification : Dire qu'on trouve tous les jours un A et un B est équivalent à dire qu'on trouve tous les jours un A et tous les jours un B

3*) aUb ≡? Ga ∧ Fb
Pas équivalentes
Justification :
	La première formule n'impose plus rien sur les A dès qu'on a trouvé un B.
	Alors que la seconde formule impose que les A continuent pendant et après le 1er B.
Contre-exemple : Si on a un B seul le 1er jour et plus rien ensuite, la première formule est vraie, mais la seconde est fausse
Remarque : La seconde formule implique la première

4*) Fa ∧ Fb ≡? F(a∧Fb) ∨ F(b∧Fa)
Équivalentes
Justification :
	Dire qu'on trouve un jour un A, et un jour un B, est équivalent à dire qu'on va
	soit trouver d'abord un A et plus tard (ou en même temps) un B,
	soit trouver d'abord un B et plus tard (ou en même temps) un A.

5) GF(a∨b) ≡? GFa ∨ GFb
Équivalentes
Justification : 
	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.

6*) aU(b ∧ Xc) ≡? aU(c ∧ X^-1 b)
Pas équivalentes
Justification : 
	La première formule dit qu'on a A jusqu'à avoir un jour B et le lendemain C.
	La seconde formule dit qu'on a A jusqu'à avoir un jour C et la veille B.
	Les 2 peuvent sembler identiques à première vue, mais il y a une légère différence :
		La première formule n'impose des A que avant le jour du B (elle n'impose pas de A le même jour que B).
		Alors que la seconde formule impose des A jusqu'au jour du C, c'est-à-dire y compris le même jour que B.
Contre-exemple : Si on a un B seul le 1er jour et un C seul le 2ème jour, alors la première formule est vraie, mais la seconde est fausse
Remarque : La seconde formule implique la première


== Exercice 4 ==

1) A n'est jamais vrai
G¬a
Autre réponse possible (formule équivalente) : ¬Fa

2) A est vrai au moins une fois
Fa

3) A est vrai une infinité de fois
GFa

4) A est vrai exactement une fois
¬aU(a ∧ XG¬a)
Traduction :
	On ne trouve aucun A, jusqu'au jour où on trouve un A, et à partir du lendemain, on ne trouve plus jamais de A
Autre réponse possible en utilisant les abréviations ^-1 :
	F (a ∧ X^-1 G^-1 ¬a ∧ XG¬a)
	Traduction de cette autre formule :
		Un jour on trouvera un A, et partir de la veille on ne trouvera aucun A avant, et à partir du lendemain on ne trouvera plus jamais de A

5) Tout A est suivi (un jour) par un B
G(a ⇒ Fb)
Remarque :
	Dans cette formule, B peut arriver le même jour que A
	Si on voulait imposer qu'un B arrive strictement après, on pouvait écrire : G(a ⇒ XFb)
	La phrase pouvait être comprise des 2 façons, et les 2 formules auraient surement été acceptées

5-bis) A est vrai exactement 2 fois
¬aU(a ∧ X(¬aU(a ∧ XG¬a)))
Explication :
	Ce n'est pas aussi effrayant que ça en a l'air : on a juste imbriqué 2 fois la formule de la question 4.
	Notons [Z] = ¬aU(a ∧ XG¬a) la formule de la question 4 qui signifie "avoir un A puis plus jamais A" = "avoir un seul A"
	A présent on veut "avoir deux A" = "avoir un A puis avoir encore un seul A" = "avoir un A puis [Z]"
	Ce qu'on peut écrire comme la formule de la question 4 en remplaçant "G¬a" (plus jamais A) par "[Z]" (avoir un seul A) : ¬aU(a ∧ X[Z])
	Ce qui donne en forme développée : ¬aU(a ∧ X(¬aU(a ∧ XG¬a)))
Remarque : 
	On peut imbriquer cette formule à l'infini pour avoir autant de A qu'on veut
	A chaque fois qu'on remplace le "G¬a" final par [Z], on ajoute un A

6) A et B sont vrais en alternance (A, B, A, B...)
(a ∧ ¬b) ∧ G(a ⇒ X(b ∧ ¬a)) ∧ G(b ⇒ X(a ∧ ¬b))
Traduction :
	Le premier jour on a A (et pas B), et chaque A est suivi le lendemain par un B (et pas de A), et chaque B est suivi le lendemain par un A (et pas de B)
Remarque :
	Comme dans l'exemple, on suppose ici que la première lettre est forcément un A.
	Si on voulait laisser la possibilité de commencer par un B, il fallait remplacer le "a" du départ par "((a∧¬b) ∨ (b∧¬a))"

7) Si on a une infinité de A, alors B est toujours vrai
(GFa) ⇒ Gb