Retour au site du LAAS-CNRS

Résumé

Les travaux présentés concernent l'utilisation de la logique linéaire (proposée par le mathématicien J.Y. Girard en 1987) pour analyser et caractériser le fonctionnement d'un réseau de Petri. Ils s'inscrivent dans une démarche type des " Sciences Pour l'Ingénieur " puisqu'il s'agit d'étudier des outils mathématiques, définis en dehors du contexte d'utilisation visé, et d'étudier leur pertinence pour l'étude et l'analyse de systèmes physiques (systèmes à événements discrets). Les principaux apports de notre travail sont : ÿ une analyse des travaux existants et l'étude des rapprochements entre comportement des réseaux de Petri et connecteurs de la logique linéaire, ÿ une proposition de représentation des réseaux de Petri en logique linéaire (équivalence entre accessibilité dans un réseau et prouvabilité en logique), ÿ la caractérisation du parallélisme effectif (structurel et dynamique) du fonctionnement d'un réseau, ÿ la caractérisation des liens de causalité dans le fonctionnement d'un réseau de Petri : il est ainsi possible de correctement prévoir son comportement temporel grâce à des dates symboliques. Le travail de preuve est conduit en utilisant le " calcul des séquents " de la logique linéaire. Ces résultats fournissent des méthodes d'analyse " orientées événements " indispensables pour la prise en compte du temps dans les réseaux de Petri, alors que la plupart des méthodes existantes sont " orientées états " (problèmes d'explosion combinatoire et de mauvaise prise en compte du parallélisme due à l'entrelacement). Le maniement du temps se faisant par des dates symboliques, les résultats obtenus sont généraux. Les perspectives concernent, d'une part, l'approfondissement de certaines notions de logique linéaire (nouveaux connecteurs, logiques non commutatives) dans le cadre des réseaux de Petri et, d'autre part, le développement du travail en cours sur le temps (dates symboliques). Enfin, l'application de ces résultats à différents domaines sera l'un des objectifs, qu'il s'agisse de l'ordonnancement et de la supervision de systèmes de production ou bien du travail coopératif dans le cadre des systèmes informatiques distribuées (thèse débutée en octobre 2000).

Abstract

This work concerns the analysis of temporal behavior of Petri nets using linear logic (proposed by J. Y. Girard in 1987). The purpose is not to directly study linear logic but to use it as a tool for describing and proving the behavior of physical systems, named " discrete-event systems ", modelized by Petri nets. Major results of this combined approach are : ¿ an analysis of the existing work and a discussion about the basic concepts of linear logic connectives and their relation to the dynamic behavior of Petri nets , ¿ a proposal of Petri nets translation into the linear logic framework : it leads to an equivalence between reachability notion in Petri net theory and sequent provability concept in linear logic, ¿ an accurate characterization of dynamical and structural concurrency relations inherent to the Petri net formalism, ¿ a method to exhibit causality relations included in a Petri net scenario : so, it is possible derive the effective temporal characterization of this scenario by means of symbolic dates. Proofs use the sequent calculus framework : symbolic dates are derived during the proof tree construction. These results add new event-oriented methods, efficient for temporal analysis, to state-oriented existing ones. They do not need to construct any state graph and so, avoid the well known disadvantages of usual state-oriented approaches : state explosion and bad concurrency characterization due to the interleaving phenomenon. As time is considered through symbolic labels, obtained results are general ones. Future developments first concern the use of supplementary linear logic notions (additive connectives, commutative systems,..) for Petri nets. The second axis regards the use of symbolic dates, generated during the proof operation, to refine some specific Petri net situations as conflicts. Last, we will apply these results to particular domains : scheduling and supervision of production systems or cooperative work through distributed computational systems (a thesis concerning this last aspect is just beginning).

Mots-Clés / Keywords

Calcul des séquents; Analyse temporelle; Réseaux de Petri; Logique linéaire; Systèmes à événements discrets; Discrete-event systems; Petri nets; Linear logic; Temporal analysis; Sequent calculus;