Formalization of Petri Nets with Individual Tokens as Basis for DPO Net Transformations - Modica, Tony; Gabriel, Karsten; Hoffmann, Kathrin (Electronic Communications of the EASST, 2011)
Reconfigurable place/transition systems are Petri nets with initial markingsand 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 runtimeis an important issue. This requires the analysis of the interaction between firing andrule-based modification. For place/transition systems this analysis has been startedexplicitly without using the general theory of M-adhesive transformation systems,because firing cannot be expressed by rule-based transformations for P/T systems inthis framework. This problem is solved in this paper using the new approach of P/Tnets with individual tokens. In our main results we show that on one hand this newapproach allows to express firing by transformation via suitable transition rules. Onthe other hand transformations of P/T nets with individual tokens can be shown tobe an instance ofM-adhesive transformation systems, such that several well-knownresults, like the local Church-Rosser theorem, can be applied. This avoids a separateconflict analysis of token firing and transformations. Moreover, we comparethe behavior of P/T nets with individual tokens with that of classical P/T nets. Ournew approach is also motivated and demonstrated by a network scenario modelinga distributed communication system.