Un graphe de fluence, ne présentant qu'une seule catégorie de noeuds, peut ètre représenté par une seule matrice. Les noeuds repèrent les lignes de la matrice, les arcs les colonnes. Pour le bigraphe qu'est le RdP (Deux catégories de noeuds), il nous faut utiliser deux matrices. Chacune des matrices définissant un système d'arcs.

  -  La matrice définissant les arcs entrants des transitions ou matrice  PRE  (précédent).
  -  La matrice définissant les arcs sortants des transitions ou matrice  POST.
 

Ecrivons les matrices  PRE  et  POST  du réseau ci-après:

             PRE                                                         POST

         t1   t2    t3    t4                                       t1   t2    t3    t4

A      1    0     0      0                                  A     0    1     0      0

B      0    1     0      0                                 B     1    0     0      0

C      0    0     1      0                                  C     3    0     0      1

D      2    0     0      1                                 D     0    0     1      0

E      0    0     0      2                                  E     0    0     1      0

A ce stade, la structure d'un réseau de Petri R peut ètre caractérisée par le quadruplet:

                              R  =  { P,  T,  PRE,  POST }

P:         Ensemble fini de places
T:         Ensemble fini de transitions
PRE:    Application  P x T ---->  N
POST:  Application   T x P ----> N

Les ensembles  P  et  T sont disjoints.

Nous notons :

              POST(ti)  :    La colonne ti de POST
              POST(pj) :    La ligne pi de POST
 

Tout élément  nij  d'une matrice sera notée:  PRE(pj,ti)  ou  POST(pi,tj)

Marquage:

Le marquage M d'un réseau (répartition de jetons dans les places) se caractérise ainsi par l'application:
         M :    P ----> N

Marquage initial:

Un RdP marqué sera caractérisé par la description  R  de ce réseau associé à son marquage initial M0.

          Rm  =  { M0, P,  T,  PRE, POST }

Evolutions du marquage d'un réseau

 On vérifie sur le réseau précédent et son marquage  M0 (matrice colonne)  que:                M0   =>    PRE(t1)
 t1 est donc  franchissable.

par contre :         M0   <   PRE(t2)     soit  t2  non validé
 

Dans ces conditions, tout nouveau marquage  M'(p)  de la place p à partir d'un précédent marquage M(p) s'obtient en effectuant l'opération:

                            M'( p )   =   M( p )  -  PRE( p, t )   +   POST( t, p )

Cette opération n'est valide que si:         M(p)  -  PRE(p, t)  >=  0
 

La généralisation à l'ensemble des places du réseau consiste à écrire:
 

                                      M'  =   M   -  PRE( t )   +   POST( t )

Au vecteur de marquage M est retranchée la colonne PRE(t) (ce sont les retraits de jetons) tandis que la colonne POST(t) est additionnée (ce sont les rajouts).

Le franchissement d'une transition  t  n'est autorisée que si après exécution de la seule soustraction

              M  -  PRE(t)  =  M"

on vérifie qu'aucun des éléments du marquage intermédiaire M" n'est négatif. Il faut tout naturellement :

              M  =>  PRE(t)

C'est la précondition de franchissement, relation notée:

              M(t>

Au franchissement de  t  correspond une relation dans   N x t x N   notée:       M(t>M'         ( m =  | P |  )
M, par le franchissement de t, amène  M'.

Pour un réseau de Petri PUR, soit: (°t  ^  t°) =  vide,   on observe que si

              PRE(p, t)  /= 0   alors    POST(p, t) = 0

et vice versa.

Dans ces conditions, puisque le franchissement d'une transition t implique l'exécution de la soustration

              POST( t )  -  PRE( t )

Il est commode de disposer directement de la matrice d'incidence  C, telle que:

              C   =    POST  -  PRE

Le réseau se définit alors à l'aide d'une seule et mème matrice.

Pour le réseau donné en début de paragraphe,on écrit :

                  t1 t2 t3 t4                                  t1 t2 t3 t4
A               0  1  0  0         1  0  0  0           -1  1  0  0
B               1  0  0  0         0  1  0  0            1 -1  0  0
C       C =  3  0  0  1    -    0  0  1  0     =    3  0 -1  1
D               0  0  1  0         2  0  0  1           0  0  1 -1
E               0  0  1  0         0  0  0  2            0  0  1 -2

                 POST       -       PRE          =          C

 Alors, l'équation de calcul du marquage  M(k+1)  à partir de  Mk  pour le  franchissement de la transition  ti  s'écrit:

              M(k+1)   =   M(k)  +  C( ti )
 

    Nota-Bene :

         L'application directe de cette équation pour le calcul du marquage consécutif au franchissement de la transition  ti permet toujours  le test  de validation de la transition ti. Il suffit de vérifier qu'aucune des  valeurs de la colonne M(k+1) est négative   (pas de jetons négatifs dans un RdP).

INVARIANCES  dans un  RdP

En programmation par exemple, on sait procéder à certaines vérifications par la méthode dites des assertions. le programme est correct si en cours d'éxecution certaines relations mathématiques sont vérifiées. S'agissant de RdP, on peut recourir aux invariants.

Preuves:

L'étude des bonnes ou mauvaises propriétés d'un réseau, ou la mise en évidence de propriétés par preuves formelles, passe souvent par l'écriture des invariants du RdP. Les preuves formelles doivent permettre la mise en évidence des caractéristiques d'un RdP annoncant telle ou telle qualité (ou défaut) du réseau.
 
 

- Invariant de PLACES :

  Un vecteur  I  de longueur égale au nombre de places du réseau (nombre de rangées de la matrice d'incidence)  est un invariant de places pour ce réseau si il est solution du système :

                      0
                      0
     C  *  I  =   .
                       .
                      0
 

- Invariant de TRANSITIONS :

  Un vecteur  J  de longueur égale au nombre de transitions du réseaux (nombre de colonnes de la matrice d'incidence  C )  est un invariant de transitions pour ce réseau si il est solution du système  :
 

                        0
                        0
    CT  *  J  =    .
                        .
                        0