HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 11:28:06 AM
Last modification on : Friday, February 4, 2022 - 3:24:11 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:29:28 PM


  • 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⟩



Record views


Files downloads