Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M-Functors

Abstract

Recently, a formal relationship between Petri net and graph transformation systems has been established using the new framework of M-functors F : (C1;M1) -> (C2;M2) between M-adhesive categories. This new approach allows to translate transformations in (C1;M1) into corresponding transformations in (C2;M2) and, vice versa, to create transformations in (C1;M1) from those in (C2;M2). This is helpful because our tool for reconfigurable Petri nets, the RONtool, performs the analysis of Petri net transformations by analyzing corresponding graph transformations using the AGG-tool. Up to now, this  correspondence has been implemented as a converter on an informal level. The formal correspondence results given by our framework make the RON-tool more reliable.

In this paper, we extend this framework to the transfer of local confluence, termination and functional behavior. In particular, we are able to create these properties for transformations in (C1;M1) from corresponding properties of transformations in (C2;M2), where (C1;M1) are Petri nets with individual tokens and (C2;M2) typed attributed graphs. This allows us to apply the well-known critical pair analysis for typed attributed graph transformations supported by the AGG-tool in order to analyze these properties for Petri net transformations.