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

== Exercice 1 ==
=== Question 1 ===

Pour mieux la comprendre, décomposons la formule : Φ = EF(a ∧ AXb)
Soit L1 = AXb : "à l'état suivant, quelle que soit la flèche qu'on prend, on aura B"
Soit L2 = (a ∧ AXb) = (a ∧ L1) : "à l'état actuel, on a A, et à l'état suivant, quelle que soit la flèche qu'on prend, on aura B"
Φ = EF(a ∧ AXb) = EF(L2) = "il existe un chemin dans lequel, un jour, on aura L2"

Cherchons d'abord les états qui vérifient L1
L1 est VRAI pour q1 : on est sûr d'avoir B le lendemain (on sera forcément en q3).
L1 est VRAI pour q2 : on est sûr d'avoir B le lendemain (on sera forcément en q5).
L1 est VRAI pour q4 et q5 : on est sûr d'avoir B le lendemain (on sera en q4 ou en q5).
L1 est FAUX pour q0 : on n'est pas sûr d'avoir B le lendemain (on pourrait être en q1 ou q2)  
L1 est FAUX pour q3 : on n'est pas sûr d'avoir B le lendemain (on pourrait être en q1) 

Cherchons à présent les états qui vérifient L2 (à la fois A et L1)
L2 est FAUX pour q0, q1 et q4, car on n'a même pas de A.
L2 est FAUX pour q3, car L1 est FAUX.
L2 est VRAI pour q2 et q5, car on a bien A et L1 est VRAI.

Cherchons enfin les états qui vérifient Φ.
Sachant que L2 est Vrai seulement pour q2 et q5.
Donc Φ = EF(a ∧ AXb) = EF(L2) = "il existe un chemin dans lequel, un jour, on ira en q2 ou en q5"
Φ est VRAI pour q2 et q5 (puisqu'on est déjà dans ces états).
Φ est VRAI pour q0 car il existe une flèche qui va direcement en q2 (et une infinité d'autres chemins pour aller en q2 ou en q5).
Φ est VRAI pour q4 car il existe une flèche qui va directement en q5 (et une infinité d'autres chemins pour aller en q2 ou en q5).
Φ est FAUX pour q1 et q3, car il n'existe aucun chemin pour aller en q2 ou q5.

Remarque :
J'ai mis beaucoup (trop ?) d'explications afin d'être compris au mieux, mais pour l'unique point que valait cette question, une réponse de 3 ou 4 lignes aurait surement été acceptée.
Dans les questions suivantes, les réponses seront plus synthétiques.

=== Question 2 ===

Ψ1 = G(b ⇒ X(a∨b))
Faux
Traduction de la formule : "Pour tous les chemins, chaque fois qu'on trouve un B, on trouve forcément A ou B le lendemain"
Justification : Pour les états q3 et q4 (accessibles depuis q0) on a B mais on n'a pas forcément A ou B le lendemain (depuis q3, on peut aller en q1, et depuis q4, on peut aller en q0). 

Ψ2 = G(a ⇒ (aUb))
Vrai
Traduction de la formule : "Pour tous les chemins, chaque fois qu'on trouve un A, on aura toujours A jusqu'à trouver un B"
Justification :
	Les états où on a A sont q2, q3 et q5. La formule nous dit qu'on doit avoir "(aUb)" dans ces états.
	Dans q3 et q5, "aUb" est trivialement vrai, puisqu'on a B.
	Dans q2, on a forcément B dès le lendemain, donc "aUb" est vrai aussi.


== Exercice 2 ==

Pour aller du plus simple au plus compliqué, commençons par comparer en LTL, puis en CTL.
Chaque fois qu'on donne une formule qui distingue 2 systèmes, c'est juste un exemple, il y en a plusieurs possibles.

=== S1 et S2 ===
* En LTL
On remarque que S1 et S2 ne lisent pas exactement les mêmes mots, signe qu'on peut les ditinguer en LTL.
S1 peut lire _abbbb... alors que S2 non.
Dans S2, si on lit A le 2ème jour, alors on lit forcément A le 3ème jour aussi.
On en déduit par exemple la formule LTL suivante qui les distingue, Fausse pour S1 et Vraie pour S2 : Xa => XXa
Réponse : On peut distinguer S1 et S2 avec la formule LTL : Xa => XXa

* En CTL
Si une formule LTL peut distinguer 2 systèmes, il suffit de la convertir de CTL en ajoutant des "A" devant chaque symbole.
Réponse : On peut distinguer S1 et S2 avec la formule CTL : AXa => (AX AXa)

=== S2 et S3 ===
On est exactment dans le même cas que pour S1 et S2.
S3 peut lire _abbbb... alors que S2 non.

* En LTL
Réponse : On peut distinguer S2 et S3 avec la formule LTL : Xa => XXa

* En CTL
Réponse : On peut distinguer S2 et S3 avec la formule CTL : AXa => (AX AXa)

=== S1 et S3 ===
* En LTL
Réponse : On ne peut pas distinguer S1 et S3 en LTL, ils sont équivalent en LTL car ils lisent exactement les mêmes mots : (_ a^w) + (_ a^* b^w)
("soit vide puis une infinité de A, soit vide puis un certain nombre de A (éventuellement zéro) puis une infinité de B")

* En CTL
On peut les distinguer en CTL, car on n'a pas toujours les mêmes choix.
Dans S3, à l'état 2, on se trouve dans une situation où on ne peut pas lire de B le lendemain.
Cette situation n'existe pas dans S1.
On peut traduire cette situation en CTL par : EX(AX ¬b)
("il existe un chemin, où demain, on sera dans un état où on ne peut plus lire de B le lendemain")
Réponse : On peut distinguer S1 et S3 avec la formule CTL "EX(AX ¬b)" qui est Vraie pour S3 et Fausse pour S1

=== S3 et S4 === (non demandé dans l'énoncé, mais probablement demandé oralement lors de l'examen)
* En LTL
Réponse : On ne peut pas distinguer S3 et S4 en LTL, ils sont équivalent en LTL pour la même raison que S1 et S3.
Remarque :
S1, S3 et S4 forment donc une classe d'équivalence en LTL : ce sont exactement les mêmes formules LTL qui sont Vraies pour les 3, et les mêmes formules LTL qui sont Fausses.
Par conséquent, on peut distinguer S4 de S2 en utilisant la même formule que pour distinguer S1 de S2, ou S3 de S2 (Xa => XXa).

* En CTL
On peut les distinguer en CTL, car on n'a pas toujours les mêmes choix.
Dans S3, à l'état 3, on se trouve dans une situation où on a A et où on ne peut pas lire de A le lendemain.
Cette situation n'existe pas dans S4.
On peut traduire cette situation en CTL par : EX(a ∧ (AX ¬a))
Réponse : On peut distinguer S3 et S4 avec la formule CTL "EX(a ∧ (AX ¬a))" qui est Vraie pour S3 et Fausse pour S4
Remarques :
	On peut évidemment distinguer S4 de S2, toujours en convertissant la formule LTL qui les distingue en CTL (AXa => (AX AXa)).
	On ne peut pas distinguer S4 de S1 : ils sont bissimilaires (on ne va pas le démontrer ici, c'est assez long).