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



== Exercice 4 ==

Notes :
* Pour les formules LTL/CTL trouvées, je mets à chaque fois celle qui me parait la plus simple, mais il y avait toujours plusieurs formules possibles.
* Les justifications et démonstrations ci-dessous donnent l'idée générale mais ne sont pas exemplaires en matière de rédaction.

=== Question 1 ===

Pour cette question, commençons par le LTL

* Peut-on distinguer S1 et S2 en LTL ?

Réponse : Oui
Formule LTL : Xa

Traduction de la formule :
Pour tous les chemins, on aura A demain
(rappel : en LTL, la formule doit être vérifiée pour tous les chemins possibles pour être vraie)

Justification :
Cette formule est vraie pour S1 car on a forcément A le lendemain.
Cette formule est fausse pour S2 car on peut ne pas avoir A le lendemain (en r2).


* Peut-on distinguer S1 et S2 en CTL ?

Réponse : Oui
Formule LTL : AXa

Traduction de la formule :
Pour tous les chemins, on aura A demain (idem formule précédente)

Justification :
Une fois qu'on a trouvé une formule en LTL, il suffit d'ajouter des quantificateurs A ("pour tout chemin") devant chaque symbole pour la transformer en formule CTL.


=== Question 2 ===

* Peut-on distinguer S2 et S3 en CTL ?

Réponse : Oui
Formule LTL : EX (AG ¬b)

Justification :
Il exite un chemin où, à partir de demain, on ne pourra plus jamais avoir de B

Justification :
Cette formule est vraie pour S2 car on peut être en r1 le 2ème jour, et à partir de là on ne pourra plus jamais avoir B.
Cette formule est fausse pour S3 car quel que soit l'état où on se trouve le 2ème jour, on garde la possibilité d'aller en B un jour.


* Peut-on distinguer S2 et S3 en LTL ?

Réponse : Non

Note :
Difficile à justifier, mais il y a plein de méthodes possibles (algos des 2 joueurs sans switch, similarité mutuelle, traces indentiques, etc)
Je ne sais pas laquelle était attendue, essayons avec la méthode des traces d'exécutions identiques.
Pour représenter les traces d'exécution, rappelons quelques points de syntaxe des expressions rationnelles :
	A* (avec l'étoile en exposant) signifie "un certain nombre de A" (y compris 0)
	A + B signifie "A ou B"
	AA* peut aussi s'écrire A+ (avec le plus en exposant) mais on ne l'utilisera pas ici pour éviter de confondre avec l'autre plus
	A^ω (A avec un oméga minuscule en exposant) signifie "une infinité de A"

Justification :
Ces 2 automates ont exactement les mêmes traces d'exécution : (AA* B)^ω + (AA* B)* A^ω
(La première partie symbolise les exécutions où on a un nombre infini de B, la seconde les exécutions où on a un nombre fini de B).
On ne peut donc pas les dinstinguer en LTL.

Remarque :
Si un état avait contenu plusieurs lettres, par exemple A et B, on aurait pu proposer de noter cet ensemble "C" pour écrire les formules de trace.
Idem si des états n'avaient contenu aucune lettre, on aurait pu noter cette situation "D" par exemple.


=== Question 3 ===

* Peut-on distinguer S3 et S4 en CTL ?

Réponse : Non

Justification :

Définissons 2 classes d'équivalence ClasseA et ClasseB.
Rangeons les états dans ces classes :
	ClasseA = {s0, t0, t1, t2, t5}
	ClasseB = {s1, t1, t4}

Les éléments de ClasseA sont bien équivalents car :
	* Ils portent tous les mêmes lettres (A)
	* Ils pointent tous les vers mêmes classes (ClasseA et ClasseB)
	
Les éléments de ClasseB sont bien équivalents car :
	* Ils portent tous les mêmes lettres (B)
	* Ils pointent tous les vers mêmes classes (ClasseA)
	
s0 et t0 sont dans la même classe, ils sont donc équivalents.
On ne peut donc pas distinguer S3 et S4 en CTL.


* Peut-on distinguer S3 et S4 en LTL ?

Réponse : Non

Justification :
On pourrait réutiliser la méthode de la question 2 avec les traces d'exécution identiques, mais il suffit de dire que si S3 et S4 ne sont pas distingables en CTL (cf point précédent) alors ils ne sont pas non plus distingables en LTL.


=== Question 4 ===

Remarque :
La formulation de la question "en déduire" sous-entend que l'on n'a plus besoin de regarder les STE, et qu'on peut déduire les réponses d'après les questions précédentes.
Commençons à nouveau par le LTL.


* Peut-on distinguer S1 et S4 en LTL ?

Réponse : Oui
Formule LTL : Xa

Jufification :
Les STE qu'on ne peut pas distinguer en LTL forment une classe d'équivalence.
D'après les questions précédentes on sait que :
S1 ≢ S2 ≡ S3 ≡ S4 => par transitivité, on en déduit que S1 ≢ S4 (si on a w ≠ x = y = z, on peut en déduire que w = z).
Donc la formule qui les distingue existe.
Et pour la trouver, il suffit de reprendre la formule qui avait dinstingué S1 et S2 : on sait déjà qu'elle était vraie pour S1, et si elle était fausse pour S2, alors elle l'est aussi pour S3 et pour S4 (puisqu'aucune formule ne peut les distinguer de S2).


* Peut-on distinguer S3 et S4 en CTL ?

Réponse : Oui
Formule CTL : AXa

Justification :
On ne peut pas reprendre le raisonnement du point précédent, car en CTL on a S1 ≢ S2 ≢ S3 ≡ S4
On ne peut rien en déduire sur l'équivalence ou non de S1 et S4 (si on a w ≠ x ≠ y = z on ne peut pas déduire si w = z ou pas).
Par contre, on peut reprendre le raisonnement de la question 1 pour transformer la formule LTL trouvée au point précédent en formule CTL (en ajoutant des quantificateur "A" sur chaque symbole).