Systeme de transition sur les ordre Partiellement complet

2.1 Construction de la catégorie des systèmes de transition sur CPO.

Dans cette section, nous mettons sur pied les éléments de base de la caté_gorie des s_ystèmes de transition sur la caté_gorie CPO.

2.1.1 Quelques définitions de base.

Habituellement, un s_ystème de transition est un couple (S, -?) formé d'un ensemble S d'états et d'une confi_guration -? sur les états (formellement, -? est ensemble de S X S). Dans ce _qui nous concerne, S est déjà enrichi d'une structure d'ordre_; nous exi_geons de la confi_guration -? _qu'elle respecte cet enrichissement_; nous proposons donc la définition suivante :

Définition 2.1. Un s_ystème de transition est un couple ( ) formé d'un opc S et

S, S //

d'un sous opc S // de S X S.

S est appelé support ou objet d'états du s_ystème.

S // est appelé structure de transition du s_ystème. Les éléments de S sont appelés états

Notations

* Lors_que (s, s') E S // , on note s S // s' et on lit 's évolue vers s' sous la transition

"

S

** lors_qu'aucune confusion n'est possible, l'on note la structure de transition S //sim-

plement par -? et le système ( ) par S.

S, S //

* * * Pour s fixé dans S, s -?:= {s' E S, s -? s'}.

Définition 2.2. Un s_ystème de transition S est dit à branchements finis si pour tout état s, s -? est fini.

Lors_que s -? est de cardinal 1, le s_ystème de transition S est dit déterministe.

Remar_que 2.1. Etant donné un s_ystème de transition S, cha_que état s de S est caractérisé par deux structures :

* l'ordre de l'opc .

** la structure de transition du s_ystème S.

Pour différencier ces structures, nous représenterons les transitions par des flèches éti_quetées d'une lettre majuscule et l'ordre par des flèches simples.

2.1.2 Quelques propriétés des systèmes de transition.

Nous proposons _quel_ques propriétés caractéristi_ques des s_ystèmes de transition. Proposition 2.1. S = (S, S //) est un s_ystème de transition si et seulement si pour toutes familles dirigées _(xi)iEI et _(yi)iEI de S, telles _que pour tout i E I, (xi, yi) E S // ,

(VS xi, VSyi)E S //

Preuve. ) Supposons S //Structure de transition et posons

L = {(xi, yi), i E I}

* Montrons _que L est une partie diri_gée de S //.L est par définition une partie de S // .

Soient (xi, yi) et (x7, y7) E L . _(xi)iEI (respectivement _(yi)iEI) étant une partie diri_gée de S,

il existe xk (respectivement yk) tel _que xi xk et x7 xk (respectivement yi yk et y7 yk).

On déduit de la définition de l'ordre composante par composante _que (xi, yi) (xk, yk) et

(xi, yi) (xk, yk). Ce _qui prouve _que L est diri_gée de S // . Comme S // est un sous

opc, il est stable pour les suprema diri_gés. Donc VS L E S // . Et d'après le lemme (1.6)

VS xi S // VSyi

?) La réciproque découle de la définition de système de transition. De manière analogue, on démontre la proposition suivante.

Proposition 2.2. S = (S, S // ) est un s_ystème de transition si et seulement si pour

toutes w-chaînes

x0 x1 ... x_n ...

et

y0 y1 ... y_n ...,

si xi S // yi alors

_VS xi S // VSyi

Nous en déduisons le corollaire suivant

Corollaire 2.1. Pour toute famille filtrante _{xi}iEI, on a :

· s'il existe aES tel _que pourtouti E I, xi S // a alors V5xi S // a_;
· s'il existe aES tel _que

xi'

.
.
.

_F#177;F

#177;

#177;#177;#177;#177;#177;#177;#177;#177; (c) CC(c)

(c) (c)

(c) (c)

(c) (c) >}>

#177;#177;#177;#177;#177;#177;#177;#177; (c)
}}}}}}}}}}}}}}}}

(c) (c)

#177;#177;#177;#177;#177;#177;#177;#177; (c) (c)

(c) (c) _ooooooo^oooooo7o7 (c) (c)

(c) (c)

(c)

#177; (c) (c)

a _O// xii

.
.

₆ A6 AOAOO

_{6 AO}

6 ₆ AOOO

_AO_O

6 6 AO

6 AOO _A'O' _{6 A}

6 A

6 AA

_{6 A}

_{6 A}

_{6 A}

₆ A

6 6 6 6 6 6 ¾6¾

.

alorsa S // V5xi

Remar_que 2.2. Nous venons de montrer _que (S, S // ) s_ystème de transition é_quivaut d'une part à

i) Pour tout ensemble I et pour toutes familles dirigées _(xi)iEI et _(yi)iEI de S, si pour tout

// V5 yi et d'autre part à

i E I, xi S // yi implique ^V5 xi S

ii)Pourtoutesw-chaînesx0=x1=...=x_n =...ety0=y1=...=y_n =...,,xi _S//yi implique ^V5 xi S // V5yi.

De cette remar_que, nous déduisons le théorème suivant.

Théorème 2.1. Soit S un s_ystème de transition. Les assertions suivantes sont é_quivalentes :

i) Pour tout ensemble I et pour toutes familles dirigées _(xi)iEI et _(yi)iEI de S, si pour tout i E I, xi S // yi, alors

ii) Pour toutes w-chaînes

V5

xi S //

V5 yi

x0 = x1 = ... = x_n = ...

et

y0 = y1 = ... = y_n = ...,

si xi S // yi alors

V5

xi S //

V5 yi