Dynamic Changes in Concurrent Systems: Modelling and Verification

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