Exercice 1

1

EG quoi qu’il arrive, il existe une prolongation sur laquelle X sera vraie tout le temps

1.1

2

1.2

3

1.3

4

1.4

5

a \RA EXb : chaque fois après a on peut faire b au tick suivant
Quand c est vrai alors le Until est vrai alors la formule est vraie, même pas besoin de regarder ce qu’il y a dans les parenthèses.

1.5

Exercice 3

1

AG(\neg(a\wedge b))

2

Avec : 3.2
AG(M \RA AXp)

3

AG : pour tout chemin
\neg EF : il n’y a pas de chemin sur lequel

\neg EF(\neg p \wedge EXr) \text{ ou } AG(EXr \RA p)

4

EF : Inévitable

EF(a \vee b)

5

Avec : 3.5
EG(p \RA EXEG\neg p)

6

Avec : 3.6

Sur tous les chemins, si j’ai p, alors dès l’instant suivant, je l’ai plus.
\neg p : plus de p après

AG(p \RA AXAG\neg p)

Exercice 4

Les colonnes avec une * sont ajoutés par le prof pour les calculs auxiliaire

Automate de gauche

a b c Ea\ U\ b Aa\ U\ b EG\ a EXc
*		 AG\ EXc AFc
*		 AG\ AFc \neg c
*		 EG\neg c
q_{0} \bot \top \top \top \top \bot \top \top \top \top \bot \bot
q_{1} \top \top \bot \top \top \bot \top \top \top \top \top \bot
q_{2} \bot \bot \top \bot \bot \bot \top \top \top \top \bot \bot
explication ? vrai si b vrai q_0 et q_2 faux car pas de a

q_1 ne laisse pas de chemin qui laissse l’état en vrai		 AFc = tout les chemins mennent évitablement vers c tout les états sont bons donc pas besoin de réfléchir Eg\neg c = existe un chemin pour lequel j’ai tout le temps \neg c

Exercice 5

a b c EXc E(EXc)\ U\ b AF\ a \varphi
q_{0} \bot \bot \top \top \top \bot \top
q_{1} \bot \bot \bot \top \top \bot \top
q_{2} \bot \bot \bot \top \top \top \top
q_{3} \bot \top \bot \bot \top \top \top
q_{4} \bot \bot \top \top \bot \bot \bot
q_{5} \top \bot \bot \bot \bot \top \top
q_{6} \bot \bot \top \bot \bot \top \top
q_{7} \top \bot \bot \bot \bot \top \top
explication ? un chemin qui reste jusqu’à b toujours dans l’avenir, j’ai a