Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M-Functors: Extended Version
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 RON-tool, 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 wellknown critical pair analysis for typed attributed graph transformations supported by the AGG-tool in order to analyze these properties for Petri net transformations.