Systeme de transition sur les ordre Partiellement complet

2.2 Notion de bissimulation entre systèmes de transition sur CPO

Une bissimulation entre deux s_ystèmes de transition ensemblistes A et B est un sous ensemble R de A X B tel _que pour tout (a, b) E R, on a :

i) Si a A // a', alors il existe b' E B tel _que b B //b' et (a', b') E R.

ii) Sib B // b', alorsilexiste a'EAtel_que a _S //a'et (a', b') ER.

En s'inspirant de cette définition, nous proposons la définition suivante de bissimulation entre s_ystèmes de transition à support un opc.

Définition 2.4. Soient S et T deux s_ystèmes de transition. On appelle bissimulation de S par T tout sous opc R de S X T tel _que, pour tout (s, t) E R, on a :

i) Sis S // s',alorsilexistet'ETtelquet T // t'et(s',t')ER.

ii) Si t T // t',alors il existe s' ES tel _que s S //s' et (s', t') E R.

2.2.1 Quelques exemples de bissimulations .

Soient S et U deux s_ystèmes de transition. Soit f : S -? U, un morphisme d'opc^s. Le résultat ci-dessous montre _que le _graphe de f est une bissimulation si et seulement si f est un morphisme de s_ystèmes de transition.

Proposition 2.4. Soient S et U deux s_ystèmes de transition. Une application continue

f : S -? U est un morphisme de s_ystèmes de transition si et seulement si son _graphe est une bissimulation.

Preuve. * Supposons _que f est un morphisme.

· Montrons _que son _graphe G (f) est une bissimulation.

* Soient (s, f (s)). Pour tout s E S et u E U, si f (s) _U //u, alors, comme f réfléchit les

transitions, il existe s' dans S tel _que f (s') = u et s _S //s'. Comme s' E S, et f est une

application, (s', f (s')) E G (f).

** Si s S // s', alors f étant un morphisme, préserve les transitions. Donc f (s) U //f (s')

*** Supposons _que G (f) soit une bissimulation et montrons _que f est un morphisme. et (s', f (s')) E G (f)

* Si s S // s', alors comme (s', f (s')) E G (f), il existe u E U tel _que f (s) U //u et

.

(s', u) E G (f) ie, u = f (s'). Donc f (s) U // f(s).

** si f (s) _U //u, alors compte tenu du fait _que (s, f (s)) E G (f), il existe s' dans S tel

_que s S />s' et (s', u) E G (f). Or (s', u) E G (f) impli_que u = f (s'). Ce _qui montre _que

f réfléchit les transitions de U. D'où le résultat.

De cette proposition, il s'en suit _que la dia_gonale du produit S X S de s_ystèmes de transition est une bissimulation de S par S car c'est le _graphe de l'identité de S. On démontre sans difficultés la proposition suivante.

Proposition 2.5. Soit R une bissimulation de S par U. R-¹ = {(u, s) telque (s, u) E R} est une bissimulation de U par S.

De cette proposition, il s'en suit _que la dia_gonale du produit S X S de s_ystèmes de transition est une bissimulation de S par S car c'est le _graphe de l'identité de S. On démontre sans difficultés la proposition suivante.

Proposition 2.6. Soit R une bissimulation de S par U. R-¹ = {(u, s) telque (s, u) E R} est une bissimulation de U par S.

Définition 2.5. Soient S et U deux s_ystèmes de transition un span est un couple d'homomorphismes de même domaine. Le dia_gramme ci-dessous illustre un span

T

ÄÄ~~^~~~~~

^@@@@@@Â@Â

S U

Tout span induit une bissimulation entre les codomaines de ses morphismes.

Le résultat suivant donne la construction d'une telle bissimulation. Dans le cas des s_ystèmes de transition ensemblistes, J.J.J.M.Rutten utilise le point de vue fonctoriel des s_ystèmes de transition pour le prouver. Nous utilisons ici le point de vue relationnel.

Proposition 2.7. Soient f : T -p S et g : T -p U deux morphismes de s_ystème de transition.

Soit K = {(f (t), g (t)) , t E T}. K est une bissimulation de S par U.

Preuve. Nous devons montrer _que K est un sous opc de S X U et satisfait les axiomes i) et ii) de la définition (2.4)

Considérons l'application ? : T -p S X U définie par ? (t) = (f (t), g (t)). f et g étant continues, ? est continue.

Donc K est un sous opc de S X U.

Il reste à montrer _que K vérifie les axiomes i) et ii).

· Soit (f (t), g (t)) E K. Si f (t) _S />s, alors comme f réfléchit les transitions, il existe t'

dans T tel _que t T /> t'; et ? (t') E K.

Par ailleurs, comme g préserve les transitions, t T /> t' impli_que g (t) T /> g (t') . Ce _qui

montre l'axiome i).

De manière analo_gue, on montre le deuxième axiome de la définition (2.4).