Symbolic Graph for Petri nets

I. Vernier

IBP-Masi 1995/04: Rapport de Recherche Masi / Masi research reports
15 pages - Février/February 1995 - Document en anglais.

PostScript : 336 Ko /Kb

Titre / Title: Symbolic Graph for Petri nets

Résumé : 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 symboliques qui définissent des ensembles de marquages des programmes instanciés. Nous prouvons que le graphe symbolique représente exactement les marquages accessibles de tous les programmes instancié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.

Abstract : In this paper we consider programs with one parameter, the number of processes, represented by Petri nets. A marked Petri net models a program with a fixed number of processes, i.e., an instantiated 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 marking for each value of the parameter. We introduce symbolic markings 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 execution of an instantiated program is represented in the symbolic graph. We show how to verify properties on the symbolic graph.

Publications internes Masi 1995 / Masi research reports 1995