Erratum

Des étudiants lecteurs perspicaces ont vu une erreur dans le document Raffinage, Model-checking et preuve...

page 10, 4.2.

P= ab* doit être écrit en FSP :

P= (a -> ETAT 1 | a -> STOP);
ETAT1 = (b -> ETAT1).

ou si on veut éviter que LTSA nous dise qu'il y a un deadlock car quand on arrive à STOP on ne peut aller plus loin,
écrire
P= (a -> ETAT 1 | a -> STOP),
ETAT1 = (b -> ETAT1 | b -> STOP).

Mais cela colle moins bien à l'expression régulière

Il faut noter que les automates adéquats aux systèmes réactifs sont les automates de Buchi (tout à l'heure j'avais un trou de mémoire), voir par exemple
http://fr.wikipedia.org/wiki/Automate_de_B%C3%BCchi
http://fr.wikipedia.org/wiki/Automate_fini