RÉSEAUX RÉENTRANTS

RÉSEAUX RÉENTRANTS

Introduction

Dans le deuxième chapitre, lors de l’étude du remplacement de sous-réseaux ouverts au moyen de l’SST-équivalence, pour pallier la difficulté de vérifier l’équivalence de deux réseaux à interface ouverte, nous avons évoqué la définition de classes particulières de réseaux pour lesquelles cette vérification serait simple. Nous avions déjà défini les réseaux à interface ouverte robustes pour obtenir la fermeture de l’ensemble des systèmes à interface ouverte par remplacement de tels sous-réseaux, et obtenir un théorème de remplacement pour les OI-systèmes. Mais cette classe ne simplifie en rien la vérification de l’équivalence. Nous avons donc cherché à définir une sous-classe des OI-réseaux robustes ayant assez de contraintes structurelles qui normalisent le comportement pour simplifier la vérification de l’SST-équivalence, et en plus, ayant de bonnes propriétés pratiques de modélisation. Nous avons alors obtenu la classe des réseaux réentrants. Les réseaux réentrants sont le résultat de la combinaison des OI-réseaux robustes définis dans le deuxième chapitre, et des réseaux à terminaison propre définis dans BRAMSfll]. Un OI-réseau robuste a un ensemble de places d’interface ITF, et un ensemble d’états stables STB, tels que STB soit un espace d’accueil accessible sans franchir des transitions sorties des places d’interface. Un réseau à terminaison propre est un réseau ayant une place initiale p¿ et une place finale pj, telles que, à partir du marquage initial où seule p, est marquée, l’état final où seule p / est marquée soit un état d’accueil. Nous généralisons alors les réseaux à terminaison propre en considérant une interface composée d’un ensemble INI de places initiales et un ensemble FIN de places finales. De plus, INI et FIN sont partitionnées en sous-ensembles, tels   qu’à un sous-ensemble PI de IAT I corresponde un sous-ensemble PF de FIN, et une marque dans une place de PI puisse aller dans n’importe quelle place de PF. Les états stables des réseaux réentrants sont alors les états terminaux qui, au lieu d’être caractérisés par « toutes les places du réseau sont vides », sont définis par: pour chaque couple (PI, PF), il existe un flot dont le support contient PIUPF, et les états stables correspondent aux états où toutes les places internes des supports sont vides. Intuitivement, un réseau réentrant s’interprète comme un serveur qui reçoit des requêtes dans des places initiales et délivre des réponses dans des places finales: ces places constituent l’interface du réseau. Plusieurs services sont disponibles, et pour chaque service, il existe plusieurs ports (places) où on peut mettre les requêtes et plusieurs ports de sortie, et il existe un flot dont le support contient les places d’interface correspondantes. La réentrance (absence de blocage quel que soit le nombre des requêtes et quel que soit leur distribution) est exprimée par une propriété d’espace d’accueil: on peut toujours vider les places intermédiaires des flots. De plus, la réponse est indéterministe, c-à-d, quel que soit l’état interne du serveur, il est toujours possible sans autre intervention de l’environnement de traiter cette requête et de lui donner n’importe quelle réponse. Mais ceci implique que tous les traitements soient indépendants: il n’y a pas de synchronisation possible entre deux exécutions d’un même service ou de deux services différents. Finalement, à travers les réseaux réentrants, nous obtenons bien des réseaux à interface ouverte robustes dont l’SST-équivalence dépend uniquement de leur structure, ce qui supprime la complexité de vérifier l’existence d’une bisimulation. Mais évidemment, il reste la complexité de vérifier la réentrance d’un réseau, qui s’exprime par une propriété d’espace d’accueil. Un autre avantage des réseaux réentrants est la possibilité de les composer par fusion de places, et ainsi de les construire hiérarchiquement: ceci nous permet d’appliquer certains résultats du chapitre III. Ainsi c’est une classe de réseaux qui se prêtent bien à l’analyse modulaire, que ce soit par remplacement de sous-réseaux ou pa r composition.

Définition et propriétés

Définition et motivations

Certaines des conditions vérifiées par un réseau réentrant sont structurelles— chemins, flots, et d’autres sont comportementales—espaces d’accueil. Les commentaires suivent la définition et font le lien avec l’interprétation intuitive d’un réseau réentrant. Définition IV-1 (Résea u réentrant) Un réseau réentrant est un triplet RN = (N;SV;M0) où (i) AT = (P, T; W) est un réseau P/T (ii) SV Ç B(P) x B(P) et SV est bijective (rappelons que B(P) est l’ensemble des parties de P). On note INI = öpi^domisv) PI l’ensemble des places initiales, et FIN = UpFecod(SV) PF l’ensemble des places finales. dom(SV) (resp. cod(SV)) forme une partition de INI (resp. FIN). ITF — INIU FIN est l’ensemble des places d’interface. INI et FIN vérifient les deux conditions suivantes: • mINI = Q • Pour tout PF G cod(SV), il n’existe pas de chemin entre deux places de PF (iii) Si SV — {(INIi,FINi);i 6 l..n}, il existe n flots fi, tels que pour tout i, le support de /,-, noté SPR„ vérifie SPRxf)ITF = ITF, = IN7,-UFIN, et ses 74 CHAPITRE IV. RÉSEAUX REENTRANTS coefficients sur IT Fi soient égaux: Vi€T , £ C(p,t)+ Y, ct(p)C(p,t) = 0 p£lTF, peSPFUXITF, oùci(p) = fi(p)/fi(p’),pf eITFi (iv) On note l’ensemble des états stables: STB = {Ai G N p \ /TF ; Vi,M| 5Pfi , y T F = 0} Pour tout m0 G N /TF , STB]P est – i {T\ITF*)-espace d’accueil de (N;M0 + m0 ) ( v ) A/o G 5T 5 (vi) Vm0 G N /rir , VA/ G ACC(AT ; M0 + m0 ) n STB, V(PJ, PF ) G SV, \/pi G PI , Vp/ G PP \ at M(pi) > 0 a/ora 35 G (T\FIN’)\M -Î-» Ai’G STB,M’lITF = M| z r F – pi + pf L’ensemble des réseaux réentrants est noté 7Lh!’. (ii) SV est un ensemble de couples d’ensembles (places initiales, places finales): chaque couple représente un service. Les ensembles des ports d’entrée et des ports de sortie des différents services sont disjoints (propriété de la partition). Les places initiales n’ont pas de transition entrée: le serveur ne peut produire une requête ni remettre une requête qu’il a commencée à traiter dans son état initial. Les places finales peuvent avoir des transitions sorties: le serveur peut reprendre un résultat et le retraiter mais il doit remettre le nouveau résultat sur le même port (pas de chemin entre places finales). Ces deux conditions sont justifiées par le lemme IV-2 qui dit que, dans une séquence menant d’un état stable à un autre, tout suffixe de cette séquence diminue le marquage des places initiales et augmente celui des places finales. (iii) Le flot représente le chemin de traitement d’une requête: les places intermédiaires du flot représentent les exécutions en cours. La propriété des coefficients implique qu’à une requête correspond une seule réponse et vice versa. Noter que les flots ne sont pas nécessairement uniques. (iv) L’ensemble des états stables (états terminaux) est défini en fonction des supports des flots.