Réseau de Petri T-temporel

Le modèle de Merlin ^[1], 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 = ${\displaystyle (R,IS)}$ tel que :

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

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

Une transition doit être sensibilisée pendant le délai minimum ${\displaystyle a_{i}}$ avant de pouvoir être tirée et ne peut rester validée au-delà du délai maximum ${\displaystyle b_{i}}$ sans être tirée ; ${\displaystyle a_{i}}$ est la date statique de tir au plut tôt et ${\displaystyle b_{i}}$ est la date de tir au plus tard de ${\displaystyle 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 ${\displaystyle E=<M,I>}$, telle que :

• ${\displaystyle M}$ est le marquage du réseau ;

${\displaystyle 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 ${\displaystyle E}$ différent la plupart du temps des intervalles initiaux. L’état initial ${\displaystyle E_{0}}$ est constitué du marquage initial ${\displaystyle M_{0}}$ et de l’application ${\displaystyle I_{0}}$ telle que :

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

L’intervalle ${\displaystyle [a_{i},b_{i}]}$ associé à la transition ${\displaystyle t_{i}}$ est relatif au moment où la transition devient validée. Supposons que ${\displaystyle t_{i}}$ soit validée à l’instant ${\displaystyle T}$, alors elle peut être franchie dans l’intervalle matérialisé par les quantités ${\displaystyle (a_{i}+T)}$ et ${\displaystyle (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 ${\displaystyle E=<M,I>}$ conduit à un nouvel état ${\displaystyle E'=<M',I'>}$ tel que :

• ${\displaystyle M'}$ est donné par l’équation classique :

   ${\displaystyle M'(p)=M(p)-Pre(p,t)+Post(p,t)}$

• ${\displaystyle I'}$ est défini ainsi :

• • pour les transitions non sensibilisées par ${\displaystyle M'}$:

   ${\displaystyle I'}$ est vide

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

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

• • pour les autres transitions :

   ${\displaystyle 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 ^[2] et Roméo ^[3],[4].

Liens externes

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

Bibliographie

1. Merlin (P.). – A Study of the Recoverability of Computer Systems. – Irvine, California, Thèse de PhD, University of California, 1974.
2. Berthomieu (D), Ribet (P.) et Vernadat (F.). – L’outil TINA : construction d’espaces d’états abstraits pour les réseaux de Petri et réseaux temporels. – MSR’2003, Hermes, 2003.
3. Gardey G, Lime D, Magnin M, et Roux OH. Roméo: A tool for analyzing time Petri nets. In 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 418-423, July 2005. Springer.
4. Lime D, Roux OH, Seidner C, et Traonouez LM. Romeo: A parametric model-checker for Petri nets with stopwatches. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), volume 5505 of Lecture Notes in Computer Science, pages 54-57, March 2009. Springer.