Extensions des réseaux de Petri

Modélisation et Représentation des Connaissances

Master IAD – MoReC – MI045

Mathieu Sassolas
mathieu.sassolas@lip6.fr

Université Pierre et Marie Curie

5 mai 2011
 Plan du cours

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9
1 Cours 9 : Réseaux de Petri
Extensions par
arcs « spéciaux »

Extension
temporelle
2 Extensions par arcs « spéciaux »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

3 Extension temporelle

2 / 21
 Plan du cours

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9
1 Cours 9 : Réseaux de Petri
Extensions par
arcs « spéciaux »

Extension
temporelle
2 Extensions par arcs « spéciaux »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

3 Extension temporelle

3 / 21
 Plan du cours

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9
1 Cours 9 : Réseaux de Petri
Extensions par
arcs « spéciaux »
Les arcs inhibiteurs
Les arcs de lecture
2 Extensions par arcs « spéciaux »
Les arcs de vidange

Extension
Les arcs inhibiteurs
temporelle
Les arcs de lecture
Les arcs de vidange

3 Extension temporelle

4 / 21
 Motivations

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9

Extensions par
arcs « spéciaux » I Les PN ne permettent pas d’exprimer des conditions très riches.
Les arcs inhibiteurs
Les arcs de lecture I Il est souvent plus simple de modéliser avec ces arcs.
Les arcs de vidange

Extension
temporelle
« De grands pouvoirs (d’expression) impliquent
Contrepartie :
de grandes indécidabilités. »
,→ De nombreux problèmes deviennent indécidables.

5 / 21
 Arcs inhibiteurs : définition intuitive

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011 Dans le cas classique, les jetons activent des transitions. Ici, ils
Cours 9 peuvent aussi les désactiver.
Extensions par
arcs « spéciaux »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

Extension
temporelle

t t est tirable t0 t 0 n’est pas tirable

6 / 21
 Définition formelle

MoReC – MI045

Mathieu Sassolas
UPMC
Un réseau de Petri avec arcs inhibiteurs est un tuple
5 mai 2011
N = hP, T , Pre, Post, Inh, m0 i où :
Cours 9

Extensions par I P est un ensemble de places,

arcs « spéciaux »
Les arcs inhibiteurs I T est un ensemble de transitions,
Les arcs de lecture
Les arcs de vidange
I Pre : P × T → N est la relation de précondition,
Extension
temporelle I Post : T × P → N est la relation de postcondition,
I Inh : P × T → (N \ {0}) ∪ {+∞} est la relation d’inhibition,
I m0 ∈ P → N est le marquage initial.

Remarque
N 0 = hP, T , Pre, Post, m0 i est un réseau de Petri classique.

7 / 21
 Sémantique

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9 I Rappel : la sémantique d’un réseau de Petri est son graphe des
Extensions par
arcs « spéciaux »
marquages : un état est un élément de P → N.
Les arcs inhibiteurs
Les arcs de lecture
I Une transition t ∈ T est active pour un marquage m si pour toute
Les arcs de vidange place p ∈ P
Extension
temporelle
Pre(p, t) ≤ m(p) < Inh(p, t)
I Si t est active pour m alors on a dans le graphe des marquages la
t
transition m →− m0 où pour toute place p,

m0 (p) = m(p) − Pre(p, t) + Post(t, p).

8 / 21
 Exemple : un test à zéro

MoReC – MI045

Mathieu Sassolas c p
UPMC

5 mai 2011
« Si c ne contient pas de jetons,
Cours 9
alors marquer q, sinon enlever
Extensions par
arcs « spéciaux » un jeton de c et marquer r »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

Extension
t0 t>
temporelle

Cas où c contient des jetons : seule

t> est activée (t0 est inhibée).

q r
Avec ce module on encode une décrémentation d’une machine à
9 / 21
deux compteurs : le problème d’accessibilité (et de couverture) est donc
indécidable pour les réseaux de Petri avec arcs inhibiteurs.
 Exemple : un test à zéro

MoReC – MI045

Mathieu Sassolas c p
UPMC

5 mai 2011
« Si c ne contient pas de jetons,
Cours 9
alors marquer q, sinon enlever
Extensions par
arcs « spéciaux » un jeton de c et marquer r »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

Extension
t0 t>
temporelle

Cas où c contient des jetons : seule

t> est activée (t0 est inhibée).

q r
Avec ce module on encode une décrémentation d’une machine à
9 / 21
deux compteurs : le problème d’accessibilité (et de couverture) est donc
indécidable pour les réseaux de Petri avec arcs inhibiteurs.
 Exemple : un test à zéro

MoReC – MI045

Mathieu Sassolas c p
UPMC

5 mai 2011
« Si c ne contient pas de jetons,
Cours 9
alors marquer q, sinon enlever
Extensions par
arcs « spéciaux » un jeton de c et marquer r »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

Extension
t0 t>
temporelle

Cas où c ne contient pas de jetons:

seule t0 est activée (t> n’a pas assez
de jetons dans c pour être tirée).

q r
Avec ce module on encode une décrémentation d’une machine à
9 / 21
deux compteurs : le problème d’accessibilité (et de couverture) est donc
indécidable pour les réseaux de Petri avec arcs inhibiteurs.
 Exemple : un test à zéro

MoReC – MI045

Mathieu Sassolas c p
UPMC

5 mai 2011
« Si c ne contient pas de jetons,
Cours 9
alors marquer q, sinon enlever
Extensions par
arcs « spéciaux » un jeton de c et marquer r »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

Extension
t0 t>
temporelle

Cas où c ne contient pas de jetons:

seule t0 est activée (t> n’a pas assez
de jetons dans c pour être tirée).

q r
Avec ce module on encode une décrémentation d’une machine à
9 / 21
deux compteurs : le problème d’accessibilité (et de couverture) est donc
indécidable pour les réseaux de Petri avec arcs inhibiteurs.
 Arcs de lecture : définition

MoReC – MI045
I Intuition: on teste le contenu d’une place sans enlever des jetons
Mathieu Sassolas
UPMC
pour autant.
5 mai 2011 I On ajoute la relation Read : P × T → N à la définition classique
Cours 9 des réseaux de Petri.
Extensions par
arcs « spéciaux »
I Une transition t ∈ T devient active pour m ssi ∀p ∈ P,
Les arcs inhibiteurs
Les arcs de lecture m(p) ≥ Pre(p, t) + Read(p, t).
Les arcs de vidange

Extension I Le marquage successeur est inchangé :

temporelle

m0 (p) = m(p) − Pre(p, t) + Post(t, p).

p p p
r r r
4 t 4 t 4
t t t
3 3 3

10 / 21 q q q
 Propriétés

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011
,→ Un arc de lecture peut toujours être simulé par autant de lectures
et d’écritures.
Cours 9

Extensions par
arcs « spéciaux » p p
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange
r r 4
Extension
4
temporelle
t ≈ t
3 4 3

q q

Il s’agit donc plus d’une facilité d’écriture que d’un nouveau modèle.
11 / 21
 Arcs de vidange: définition

MoReC – MI045
I Intuition: on ne teste pas la place, mais on enlève tous les jetons
Mathieu Sassolas
UPMC qui s’y trouvent.
5 mai 2011
I On ajoute la fonction Fl : T × P → {>, ⊥} à la définition classique
Cours 9 des réseaux de Petri.
Extensions par
arcs « spéciaux » I La condition de tir est inchangée : ∀p ∈ P, m(p) ≥ Pre(p, t).
Les arcs inhibiteurs t
Les arcs de lecture − m0 avec, pour p ∈ P
I Pour t active pour m, on a m →
Les arcs de vidange

Extension 0 si Fl(t, p) = >
temporelle m0 (p) =
m(p) − Pre(p, t) + Post(t, p) si Fl(t, p) = ⊥

p p p
r r r
t t
t t t
3 3 3

12 / 21
q q q
 Propriétés et exemple

MoReC – MI045

Mathieu Sassolas t1 t2 t3 t4 t1 t1 t2 t4 t1 t2 t3 t4 t1 t1 t2 t3 t3 t4 . . .
UPMC

5 mai 2011

Cours 9 t1
Extensions par
arcs « spéciaux »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

Extension
temporelle
t4 t2

t3

I Le problème de couverture est décidable dans les réseaux de Petri

avec arcs de vidange.
13 / 21
I Le problème de savoir si un tel réseau est borné est indécidable.
 Plan du cours

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9
1 Cours 9 : Réseaux de Petri
Extensions par
arcs « spéciaux »

Extension
temporelle
2 Extensions par arcs « spéciaux »
Les arcs inhibiteurs
Les arcs de lecture
Les arcs de vidange

3 Extension temporelle

14 / 21
 Motivations

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9 ,→ Les mêmes que ce qui motive la définition des automates

Extensions par
arcs « spéciaux »
temporisés.
Extension
temporelle I Il y a plusieurs définitions possible pour mettre du temps sur les
réseaux de Petri.
I On présente ici les Réseaux de Petri Temporels (Time Petri Nets)
de [Merlin,1974].
On prend une transition dans un intervalle de temps après qu’elle
fût activée : à chaque transition est associée une horloge.

15 / 21
 Définition

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011
Un réseau de Petri temporel est un tuple
Cours 9
N = hP, T , Pre, Post, eft, lft, m0 i où :
Extensions par
arcs « spéciaux »

Extension
I P est un ensemble de places,
temporelle
I T est un ensemble de transitions,
I Pre : P × T → N est la relation de précondition,
I Post : T × P → N est la relation de postcondition,
I eft : T → Q≥0 est le délai de tir au plus tôt de t.
I lft : T → Q≥0 ∪ {+∞} est le délai de tir au plus tard de t.
I m0 ∈ P → N est le marquage initial.

16 / 21
 Sémantique

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011
I Intuition : On ne peut tirer une transition que si on a attendu un
Cours 9 temps dans l’intervalle de tir depuis la dernière activation de la
Extensions par
arcs « spéciaux »
transition. Si on atteint le délai de tir au plus tard, on doit tirer la
Extension
transition.
temporelle
I Une configuration du réseau est une paire (m, v ) où m est un
marquage et v : T → R≥0 est une valuation des horloges de
chaque transition.
I On dit d’une transition t 0 qu’elle est nouvellement activée par t si
• t 0 est activée par le marquage après le tir de t et
• soit t 0 était désactivée avant la production des jetons par t, soit
t = t0.
On change l’atomicité des transitions d’un réseau de Petri classique.

17 / 21
 Sémantique

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011
I Pas de temps de durée d :
Cours 9

Extensions par
• si pour t ∈ T telle que t est activée par m, on a v (t) + d ≤ lft(t),
arcs « spéciaux » d
• alors (m, v ) −
→ (m, v + d)
Extension
temporelle I Pas discret par la transition t :
• si t est activée par m (au sens classique : ∀p ∈ P, m(t) ≥ Pre(p, t))
et eft(t) ≤ v (t) ≤ lft(t),
t
→ (m0 , v 0 ) où m0 est successeur au sens classique de m
• alors (m, v ) −
par t (∀p ∈ P, m0 (p) = m(p) − Pre(p, t) + Post(t, p)), et

si t 0 est nouvellement activée par t


0
∀t 0 ∈ T , v 0 (t 0 ) = 0
v (t ) sinon

18 / 21
 Exemple

MoReC – MI045

Mathieu Sassolas
t3
UPMC

5 mai 2011

Cours 9

Extensions par
arcs « spéciaux » t1 t2 t5
Extension
temporelle
[0, 6] [4, +∞[ [2, 5]

t4 t6
[0, 2] [3, 7]

4 t2 2 t5 0 t1 2.17 t2 2 t5 0.77 t6 1.54 t4 3.73 t1 2.12 t6 0.87 t4 12.8 t2

2 t3 4.38 t6 1.11 t4 3.76 t1

19 / 21
 Propriétés

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9

Extensions par I Les problèmes d’accessibilité et du caractère borné d’un réseau de

arcs « spéciaux »
Petri temporel sont indécidables.
Extension
temporelle
I Une construction analogue au graphe des régions dans le cas des
automates temporisés permet d’abstraire le temps
,→ Ce graphe peut par contre être infini si le réseau n’est pas borné.
I Les TPN bornés peuvent être traduits en un ensemble synchronisé
d’automates temporisés.

20 / 21
 Conclusion

MoReC – MI045

Mathieu Sassolas
UPMC

5 mai 2011

Cours 9 I Les extensions des réseaux de Petri sont assez utile pour modéliser
Extensions par
arcs « spéciaux »
des systèmes.
Extension I Elles sont souvent moins performantes du point de vue de la
temporelle
vérification.
I Il existe tout de même des outils sur ces extension : par exemple
TINA ou encore Roméo (à découvrir en TME si les ordinateurs le
supportent).

,→ Examen le 26 mai de 15h45 à 17h45 en salle 46-00/103.

21 / 21