Analyse algorithmique des réseaux de Petri : vérification d'espace d'accueil, systèmes de réécriture
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
The main motivation of this thesis is the conception of automatic analysis techniques of Petri nets. The thesis deals with two themes: verification of home space, application of techniques based on rewriting systems. A home space is a always reachable set of markings whatever the evolution of the system may be. This property allows, for instance, verifying that idle state of process is always accessible. It also allows validating behavioural properties (such as liveliness). In the first part, we prove that the property "a finite union of linear sets having the same periods is a home space" is decidable. A semi-decision algorithm checking a home space is presented in the second part. An approach using marking sets leads to especially efficient results. In one stage, it verifies that the home space is reachable from all the markings of a marking set. A class of marking sets which can be easily manipulated is defined (delimited sets). The resulting text is short; nevertheless it precisely indicates how to reach the home space from a given marking. The third part links Petri nets and abstract data types. A representation of Petri nets into a set of equations is established. Some properties (boundless, confluence) are directly related to properties of the rewriting system obtained by completion "à la Knuth-Bendix" of the equations. Some other properties (quasi-liveliness, finite termination, accessibility of a marking. . . ) can be validated by the convergence of the rewriting system obtained by adding the equation corresponding to the property to be proved. Proofs which usually require manual elaborated induction principles can be automatically completed this way.
Abstract FR:
La motivation essentielle de cette thèse est la conception de techniques d'analyse automatique des réseaux de Petri. Elle est articulée autour de deux thèmes : la vérification de la propriété d'espace d'accueil et l'usage des techniques liées aux systèmes de réécriture. Un espace d'accueil est un ensemble de marquages toujours accessible quelle que soit l'évolution du système. Cette propriété permet, par exemple, de vérifier que l'état d'inactivité des processus est toujours accessible. Elle permet aussi de valider des propriétés comportementales (telle la vivacité). Dans la première partie de cette thèse, nous démontrons que la propriété "la réunion finie d'ensembles linéaires ayant mêmes périodes est un espace d'accueil" est décidable. Un algorithme de semi-décision vérifiant un espace d'accueil est présenté dans la deuxième partie. Un traitement par ensemble de marquages permet d'obtenir des résultats particulièrement probants. En une seule étape, on vérifie que l'espace d'accueil est accessible à partir de tous les éléments d'un même ensemble. Pour cela, une classe d'ensembles de marquages facilement caractérisables est définie: les ensembles délimités. Le texte résultant de l'analyse est court, il indique cependant avec précision comment atteindre l'espace d'accueil à partir d'un marquage donné. La troisième partie lie les réseaux de Petri et l'approche des types abstraits algébriques. Une représentation des réseaux de Petri en un ensemble d'équations est établie. Certaines propriétés (caractère borné, confluence) sont reliées directement au système de réécriture obtenu après complétion des équations "à la Knuth-Bendix". D'autres propriétés (quasi vivacité, terminaison finie, accessibilité d'un marquage. . . ) peuvent être prouvées par la convergence du système de réécriture auquel est ajoutée l'équation traduisant la propriété à valider. Des preuves nécessitant d'ordinaire l'élaboration manuelle d'un principe d'induction peuvent être ainsi automatiquement effectuées.