Réseau de Petri T-temporel

Le modèle de Merlin , communément appelé réseau de Petri t-temporel, a été conçu pour l’étude des problèmes de recouvrement pour les protocoles de communication. Dans ce modèle, à chaque transition est attachée une contrainte temporelle de type intervalle, et non plus ponctuelle comme dans le modèle t-temporisé.

Définition

réseau de Petri t-temporel

Un exemple de réseau de Petri t-temporel

Un réseau de Petri t-temporel est un doublet = $(R,IS)$ tel que :

• $R$ est un réseau de Petri marqué
• $IS$ est l’application intervalle statique telle que :

$IS:T\to Q^{+}\times (Q^{+}\cup (+\infty ))$
$t_{i}\to IS(t_{i})=[a_{i},b_{i}]$ avec $a_{i}\leq b_{i}$

Une transition doit être sensibilisée pendant le délai minimum $a_{i}$ avant de pouvoir être tirée et ne peut rester validée au-delà du délai maximum $b_{i}$ sans être tirée ; $a_{i}$ est la date statique de tir au plut tôt et $b_{i}$ est la date de tir au plus tard de $t_{i}$ .

États et règles de tir: Ici encore, la notion d’état est utilisée pour caractériser la situation du réseau t-temporel à un instant donné.

État d’un réseau de Petri t-temporel

L’état d’un réseau de Petri t-temporel est défini par une paire $E=<M,I>$, telle que :

• $M$ est le marquage du réseau ;

$I$est une application qui associe à chaque transition du réseau un intervalle de temps pendant lequel elle est franchissable.

Les intervalles de tir associés aux transitions du réseau dans un état $E$ différent la plupart du temps des intervalles initiaux. L’état initial $E_{0}$ est constitué du marquage initial $M_{0}$ et de l’application $I_{0}$ telle que :

• si $M_{0}>Pre(k)$ alors $I_{0}(k)=IS(k)$ ;
• sinon $I_{0}(k)=\varnothing$.

L’intervalle $[a_{i},b_{i}]$ associé à la transition $t_{i}$ est relatif au moment où la transition devient validée. Supposons que $t_{i}$ soit validée à l’instant $T$, alors elle peut être franchie dans l’intervalle matérialisé par les quantités $(a_{i}+T)$ et $(b_{i}+T)$, sauf si elle est désensibilisée à cause du franchissement d’une autre transition avec laquelle elle est en conflit.

D’après les règles de fonctionnement de ce modèle, on ne commence à compter le temps que si la transition est validée. Ainsi une marque peut rester jusqu’à l’infini dans une place en amont d’une transition de synchronisation (jusqu’à la validation de cette transition). C’est la dernière marque qui valide une transition de synchronisation qui fixe l’échéance de tir de cette transition.

Le tir d’une transition t sensibilisée à l’instant depuis l’état $E=<M,I>$ conduit à un nouvel état $E'=<M',I'>$ tel que :

• $M'$ est donné par l’équation classique :

   $M'(p)=M(p)-Pre(p,t)+Post(p,t)$

• $I'$ est défini ainsi :

• • pour les transitions non sensibilisées par $M'$:

   $I'$ est vide

• • pour les transitions sensibilisées par $M'$ et pas en conflit avec $t$:

   $I'=[max(0,a_{k}-\tau ),b_{k}-\tau ]$

• • pour les autres transitions :

   $I'=I$

Ainsi, la règle de franchissement, imposant que l’horloge locale associée à chaque transition du modèle ne soit déclenchée qu’à la validation logique de celle-ci, ne permet pas la prise en compte de façon naturelle du phénomène de synchronisation sous obligation.

Néanmoins, le formalisme réseau de Petri t-temporel reste probablement le meilleur outil de spécification des protocoles et de processus temporels. De nombreux résultats autour de ce formalisme sont disponibles dans la littérature. Le fonctionnement au plus tôt est notamment toujours réalisable. Enfin, une instrumentation logicielle performante permet la modélisation, l’analyse et la simulation grâce aux outils logiciels TINA et Roméo .

Liens externes

• Réseau de Petri
• Réseau de Petri temporel
• Réseau de Petri temporisé
• Réseau de Petri P-temporel