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



== Exercice 3 ==

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-q0-q0-q0-... 

2) X(a∨b)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, à l'étape 2, on aura A ou B
Justification : Vrai car à la 2ème étape, on soit on est resté en q0 (alors A est vrai) soit on est passé dans q1 (alors B est vrai)

3) aWb
Vrai
Rappel : 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écutions sauf celle où on reste toujours sur q0, 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".

4) Ga ⇒ G¬b
Vrai
Traduction de la formule LTL : Dans toutes les exécutions où on a toujours A, on n'aura jamais B
Justification :
	La seule exécution qui respecte la condition "toujours A" est celle qui reste en q0
	Et cette exécution respecte également la condition "jamais B"
	Donc cette implication est Vraie

5) Ga
Faux
Traduction de la formule LTL : Dans toutes les exécutions, on a toujours A
Justification : Vrai, car à part celle qui reste en q0, aucune excution ne respecte cette condition : on n'a pas A dès qu'on arrive en q1

6) (GF¬a) ⇒ (GFc)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, si on a une infinité de fois "pas A", alors on a une infinité de fois C
Justification : 
	La première partie de l'implication est vraie pour toutes les exécutions, sauf celle qui reste toujours sur q0 :
		Car une fois passé en q1, on ne trouve plus de boucle qui permette d'avoir toujours en A
		Au mieux, on aura A un jour sur 2, en q2
		Donc on aura bien une infinité de jours sans A
	La seconde partie de l'implication est vraie aussi pour les mêmes exécutions :
		Une fois qu'on a atteint q1, on est obligé d'être au moins un jour sur 2 dans un état qui porte un C
	Donc l'implication est bien Vraie pour toutes les exécutions
	
7) (GF¬a) ⇒ (GFb)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, si on a une infinité de fois "pas A", alors on a une infinité de fois B
Justification : Vrai, exactement pour les mêmes raisons que dans la question précédente