I. Vernier
Symbolic Graph for Petri nets

 Dans  cet  article  nous  considérons  des  programmes  avec  un
paramètre, le nombre de processus, représentés par des réseaux de
Petri.  Un réseau de Petri marqué est un programme avec un nombre
fixé de processus, c-a-d un programme instancié. Nous donnons  un
algorithme  pour  construire  un graphe symbolique qui représente
les graphes d'accessibilité d'un réseau de Petri avec  un  nombre
infini de marquage initiaux. Chaque marquage initial correspond à
une valeur du paramètre. Nous introduisons les marquages  symbol­
iques  qui  définissent des ensembles de marquages des programmes
instanciés. Nous prouvons que le graphe symbolique représente ex­
actement les marquages accessibles de tous les programmes instan­
ciés. Chaque exécution d'un programme instancié  est  représentée
dans  le  graphe  symbolique.  Nous montrons comment vérifier des
propriétés sur le graphe symbolique.
 In this paper we consider programs with one parameter, the  num­
ber  of  processes, represented by Petri nets. A marked Petri net
models a program with a fixed number of processes, i.e.,  an  in­
stantiated  program.  We  give  an  algorithm to build a symbolic
graph that represents the reachability graphs of a Petri net with
an infinite number of initial markings. There is an initial mark­
ing for each value of the parameter. We introduce symbolic  mark­
ings  that  define  sets of markings of instantiated programs. We
prove that the symbolic graph represents  exactly  the  reachable
markings  of  all the instantiated programs. Each possible execu­
tion of an instantiated program is represented  in  the  symbolic
graph. We show how to verify properties on the symbolic graph.