Ensemble des marquages accessibles \mathcal{A}(R, M_{0})

Pour l’instant, on a juste défini les sommets, on doit définir désormais les transitions

Définition (1) : Graphe de marquages (accessible)

Pour un réseau de Petri marqué <R, M_{0}>, le graphe des marquages accessibles G(R, M_{0}) = <\mathcal{A}(R, M_{0}, \ra, L)>

• \mathcal{A}(R, M_{0}) est l’ensemble des états
• L est un ensemble de labels (noms) des transitions
• \ra \subseteq \mathcal{A}(R, M_{0}) \times L \times \mathcal{A}(R, M_{0}) tel que \forall M_{1} M_{2} \text{ et } \forall t \in L \in \mathcal{A}(R, M_{0}) : M_{1} \xrightarrow{t} M_{2} \Leftrightarrow M_{1} [t M_{2}

Définition (2)

G(R, M_{0}) est un STE : <Q, q_{0}, Act, \ra, AP, \mathcal{L}>

• Q = \mathcal{A}(R, M_{0})
• Q_{0} = M_{0}
• Act = T (noms de transitions)
• \ra \subseteq Q \times Act \times Q tel que q\xrightarrow{t}q' ssi q = M_{1} et q' = M_{2} et celle de la définition (1)
• AP (propositions atomiques) : Cond(M), M\in \N^{p}
• \mathcal{L} : Q \ra AP

Les “bonnes” propriétés d’un réseau de Petri

Dans <R, M_{0}>.

La vivacité

Transition vivace
Quel que soit mon marquage actuel, j’ai une manière de tirer la transition t maintenant ou dans le futur.
“Possibilité de sensibilisé depuis n’importe quelle transition.”
Une transition t est vivante si et seulement si \forall M \in G(R, M_{0}) \exists\ \sigma \in L^{*} tel que M\xrightarrow{\sigma}M' \wedge M'[t\rangle

\RA Un réseau qui ne se bloque pas \neq un réseau vivant

Un réseau est vivant ssi toutes ses transitions sont vivantes.

Non-blocage

<R, M_{0}> est sans blocage ssi si \forall M\in G-R, M_{0} \exists t \in L : M[t\rangle

Un non-blocage n’implique pas une vivacité.

Sans blocage et non vivant :
Réseau zombie : vivant, mais bloquant (mort-vivant) : \RA il faut qu’il y ait au moins une transition.

Quasi-vivacité

Je peux sensibiliser ma transition au moins une fois.
Une transition quasi vivante t est quasi-vivante ssi \exists M \in G(R, M_{0}) : M[t\rangle

Un réseau de Petri est quasi vivant ssi toutes ses transitions le sont.

Quasi vivant et bloquant :

Réinitialisibilité

Quel que soit le marquage accessible, il y a possibilité dans le marquage initiale M_{0}

Réseau de Petri : R, M_0 est réinitialisable si et seulement si :

Définition faible

\forall M \in G(R, M_{0}) \exists \sigma \in L^{*} : M \xrightarrow{\sigma} M_{0}
Dans ce cas, un réseau réinitialisable peut être bloqué sur son marquage initiale.

Définition forte

L^{+} : Sigma non-vide

\forall M \in G(R, M_{0}) \exists \sigma \in L^{+} : M \xrightarrow{\sigma} M_{0}

Dans ce cas, un réseau réinitialisable est non bloquant.

Réseau borné

Place bornée
Une place p est bornée ssi \exists k \in \N tel que \forall M \in G(R, M_{0}) : M(p) \leq k

Un réseau de Petri est borné ssi toutes ses places le sont.

Réseau non borné, mais réinitialisable :

• Réseau borné ? Oui
• Réseau réinitialisable ? Oui
• Réseau vivant ? Non

Tina