Formalization of petri nets with individual tokens as basis for DPO net transformations

Abstract

Reconfigurable place/transition systems are Petri nets with initial markings and a set of rules which allow the modification of the net structure during runtime. They have been successfully used in different areas like mobile ad-hoc networks. In most of these applications the modification of net markings during runtime is an important issue. This requires the analysis of the interaction between firing and rule-based modification. For place/transition systems this analysis has been started explicitly without using the general theory of M-adhesive transformation systems, because firing cannot be expressed by rule-based transformations for P/T systems in this framework. This problem is solved in this paper using the new approach of P/T nets with individual tokens. In our main results we show that on one hand this new approach allows to express firing by transformation via suitable transition rules. On the other hand transformations of P/T nets with individual tokens can be shown to be an instance ofM-adhesive transformation systems, such that several well-known results, like the local Church-Rosser theorem, can be applied. This avoids a separate conflict analysis of token firing and transformations. Moreover, we compare the behavior of P/T nets with individual tokens with that of classical P/T nets. Our new approach is also motivated and demonstrated by a network scenario modeling a distributed communication system.