Dynamic Changes in Concurrent Systems: Modelling and Verification

Eric Badouel 1 Javier Oliver 2
1 PARAGRAPHE - Parallelism and Graphs
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : In this paper we address the issues of modelling and verification of concurren- t systems subject to dynamic changes using Petri net formalisms. As far as the expressivity of the model is concerned a built-in and decentralized mechanism for handling changes is looked for. At the same time the basic decidable properties of Petri nets (Place Boundedness, Reachability, Deadlock, and Liveness) should remain decidable for the extended model. The gain in terms of modelling power is usually paid by a loss of decidable properties. A trade-off needs to be found between expressivity and computability. In a previous study we have introduced a class of high level Petri nets, called reconfigurable nets, that can dynamically modify their own structure by rewriting some of their components. These nets were used for modelling computer supported cooperative work (CSCW) and more precisely workflow systems. In this study we restrict our attention to the subclass of reconfigurable nets, termed reversible, whose structure modifying rules are formally inversible. Such a net may be viewed as the cascaded composition of an automaton with a parametric Petri net; and under some additional assumption it is equivalent to a stratified Petri net. Place boundedness, reachability, deadlock, and liveness are decidable properties of reversible reconfigurable nets. From a practical point of view however the choice of a particular model (Petri nets, selfmodifying or stratified Petri nets, reconfigurable nets ...) depends strongly on the nature of the problem to be modelized.
Type de document :
[Research Report] RR-3708, INRIA. 1999
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:28:06
Dernière modification le : vendredi 23 mars 2018 - 14:01:56
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:29:28



  • HAL Id : inria-00072960, version 1



Eric Badouel, Javier Oliver. Dynamic Changes in Concurrent Systems: Modelling and Verification. [Research Report] RR-3708, INRIA. 1999. 〈inria-00072960〉



Consultations de la notice


Téléchargements de fichiers