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

Abstract: Recently, a formal relationship between Petri net and graph transforma-tion systems has been established using the new framework of M-functors F: (C1,M1) → (C2,M2) between M-adhesive categories. This new approach al-lows 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 func-tional behavior. In particular, we are able to create these properties for transforma-tions 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 at-tributed graph transformations supported by the AGG-tool in order to analyze these properties for Petri net transformations