Flexible Independence of Net Transformations and Token Firing in the Cospan DPO Approach
Kathrin Hoffmann, Julia Padberg, Hartmut Ehrig, Frank Hermann · 2011
The double pushout (DPO) approach for graph transformation has been applied al- ready to Petri nets in order to model rule based transformations of the net structure. Recently, as alternative to the classical DPO approach, the cospan DPO approach has been proposed where rules are cospans instead of spans. Although the cospan DPO approach has been shown to be equivalent to the classical DPO approach, there are several advantages using the cospan DPO approach especially for Petri nets. Roughly spoken, in the classical DPO approach the intermedi- ate net obtained by rule application can be full of holes like Swiss cheese, while in the cospan DPO approach this net includes the source net and the target net. Thus, on the one hand several properties can be formulated in a more intuitive way and on the other hand some aspects can be investigated that have escaped our attention in the classical DPO approach. In this paper we pre- sent main results of a line of research 1 concerning the independence of net transformations and token firing. In more detail we apply the cospan DPO approach to Petri nets and give not only sufficient but also necessary conditions for the execution of a transformation step and a firing step leading to the same result.