Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M-Functors Electronic Communications of the EASST Volume 51 (2012) Proceedings of the 5th International Workshop on Petri Nets, Graph Transformation and other Concurrency Formalisms (PNGT 2012) Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M -Functors Maria Maximova, Hartmut Ehrig and Claudia Ermel 12 pages Guest Editors: Julia Padberg, Kathrin Hoffmann Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M -Functors Maria Maximova, Hartmut Ehrig and Claudia Ermel Institut für Softwaretechnik und Theoretische Informatik Technische Universität Berlin, Germany mascham@cs.tu-berlin.de, ehrig@cs.tu-berlin.de, claudia.ermel@tu-berlin.de 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. Keywords: M -adhesive transformation system, graph transformation, Petri net transformation, confluence, termination, functional behavior 1 Introduction Reconfigurable Petri nets have been introduced to enable formal modeling of controlled reconfig- uration of dynamic systems, which has proven to be useful for application areas such as computer supported cooperative work [HM10] or mobile networks [PEH07]. Petri net reconfiguration is modeled in a rule-based setting, where the structure of place/tran- sition nets may be changed by applying net transformation rules [EHP+08, PEHP08]. The ap- proach is related to graph transformation [EEPT06], where structural changes are modeled in the double-pushout (DPO) approach for the category of (typed, attributed) graphs, and has been gen- eralized to M -adhesive categories, which rely on a class M of monomorphisms, generalizing weak adhesive HLR categories. The DPO approach is a suitable description of transformations leading to results like the Local Church-Rosser, Parallelism, Concurrency, Embedding, Exten- sion, and Local Confluence Theorems [EEPT06]. The well-established tool AGG [AGG09] supports modeling and analysis of (typed, attributed) graph transformation systems. 1 / 12 Volume 51 (2012) mailto:mascham@cs.tu-berlin.de mailto:ehrig@cs.tu-berlin.de mailto:claudia.ermel@tu-berlin.de Transfer of Local Confluence and Termination between PN and GT Systems In our previous paper [MEE11], we have proposed formal criteria ensuring a semantical cor- respondence of reconfigurable Petri nets and their corresponding representations as graph trans- formation systems. The aim of our previous work was to establish a formal basis allowing us to translate Petri net transformations into graph transformations and, vice versa, to create Petri net transformations from graph transformations such that the behavior of Petri net transformations can be simulated by simulating their translation using the graph transformation tool AGG. In [MEE11], we established the new framework of M -functors F : (C1,M1)→(C2,M2) be- tween M -adhesive categories. This framework 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). Building on this previous work, we now extend our framework to allow the analysis of in- teresting properties of Petri net transformation systems, like termination, local confluence and functional behavior, in addition to parallel and sequential independence, using corresponding re- sults and analysis tools like AGG for graph transformation systems. We have shown in [MEE11] that we can create these properties for transformations in (C1,M1) from corresponding proper- ties of transformations in (C2,M2), where (C1,M1) are Petri nets with individual tokens and (C2,M2) typed attributed graphs. This allows us in particular 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. In our tool for reconfigurable Petri nets, (the RON-tool [RON07, BEHM07] for modeling and analyzing Reconfigurable Object Nets), the analysis of Petri net transformations is performed by analyzing corresponding graph transforma- tions using AGG. Up to now, this correspondence has been implemented as a converter from RON models to graph transformation systems on an informal level. The formal correspondence results for analysis properties in this paper make our tool environment much more reliable. The paper is structured as follows: Section 2 introduces the basic notions of M -adhesive transformation system and M -functor to define a formal relationship between two different M - adhesive categories. In Section 3, we recall the definition of the M -functor between Petri net and graph transformation systems from [MEE11]. The main new results are elaborated in Section 4 (F -transfer of local confluence), and in Section 5 (F -transfer of termination and functional behavior). In Section 6, we compare our approach to related work, conclude the paper and give an outlook to future research directions. For detailed proofs see [MEE12]. 2 Basic Concepts In this section we concentrate on some basic concepts and results that are important for our approach. Our considerations are based on the framework of M -adhesive categories. An M - adhesive category [EGH10], consists of a category C together with a class M of monomor- phisms such that the following properties hold: C has pushouts (POs) and pullbacks (PBs) along M -morphisms, M is closed under isomorphisms, composition, decomposition, POs and PBs, and POs along M -morphisms are M -VK-squares (see Figure 1), i.e. the VK-property holds for all commutative cubes, where the given PO with m ∈ M is in the bottom, the back faces are PBs and all vertical morphisms a,b,c and d are in M . The VK-property means that the top face is a PO iff the front faces are PBs. Proc. PNGT 2012 2 / 12 ECEASST A B C D A′ B′ C′ D′ mf g n m′ f ′ g′n ′ a b c d Figure 1: M -VK-square The concept of M -adhesive categories generalizes that of ad- hesive [LS04], adhesive HLR, and weak adhesive HLR categories [EEPT06]. The category of typed attributed graphs and several categories of Petri nets are weak adhesive HLR (see [EEPT06]) and hence also M -adhesive. A set of transformation rules in an M -adhesive category constitutes an M -adhesive transformation system [EGH10]. Definition 1 (M -Adhesive Transformation System) Given an M -adhesive category (C,M ), an M -adhesive transformation system AS = (C,M ,P) has a set P of productions of the form ρ = (L l←− K r−→ R) with l,r ∈ M . A direct transformation G ρ,m =⇒ H via ρ and match m consists of two pushouts according to the DPO approach [EEPT06]. We use the notion of an M -functor [MEE11] to define a formal relationship between two different M -adhesive transformation systems. Definition 2 (M -Functor) A functor F : (C1,M1) → (C2,M2) between M -adhesive categories is called M -functor if F (M1)⊆ M2 and F preserves pushouts along M -morphisms. Given an M -adhesive transformation system AS1 = (C1,M1,P1), we want to translate trans- formations from AS1 to AS2 = (C2,M2,P2) with translated productions P2 = F (P1) and, vice versa, we want to create transformations in AS1 from the corresponding transformations in AS2. This can be handled by Theorem 1 below, shown in [MEE11]. By definition, each M -functor F : (C1,M1)→(C2,M2) translates each production ρ = (L l← K r→ R) in P1 with l,r ∈ M1 into F (ρ) = (F (L) F (l) ← F (K) F (r) → F (R)) in P2 = F (P1) with F (l),F (r) ∈ M2 and each direct transformation G ρ,m =⇒ H in AS1 given by DPO (1)+(2) into a direct transformation F (G) F (ρ),F (m) =⇒ F (H) in AS2 given by DPO (3)+(4). L K R G D H (1) = (2) = l r m k ⇒ F (L) F (K) F (R) F (G) F (D) F (H) (3) = (4) = F (l) F (r) F (m) k′ Vice versa, we say F creates direct transformations, if for each direct transformation F (G) F (ρ),m′ =⇒ H′ in AS2 there is a direct transformation G ρ,m =⇒ H in AS1 with F (m) = m′ and F (H)∼= H′ leading to F (G) F (ρ),F (m) =⇒ F (H) in AS2. In the following, we provide two conditions in order to show creation of direct transformations and transformations, i.e. sequences of direct transformations written G ∗⇒ H. Theorem 1 (Translation and Creation of Transformations) Each M -functor F : (C1,M1)→ (C2,M2) translates (direct) transformations. Vice versa, F creates (direct) transformations if we have the following two conditions: 3 / 12 Volume 51 (2012) Transfer of Local Confluence and Termination between PN and GT Systems • (F creates morphisms): For all m′ : F (L) → F (G) in (C2,M2) there is exactly one morphism m : L → G with F (m) = m′. • (F translates initial pushouts): (C1,M1) has initial pushouts and for each initial pushout (1) over m : L → G also (2) is initial pushout over F (m) in (C2,M2). B (1) L C G b m ⇒ F (B) (2) F (L) F (C) F (G) F (b) F (m) The proof for Theorem 1 is given in [MEE11]. Moreover, it is shown under the same as- sumptions that F translates and creates parallel and sequential independence of transformations. Concerning the definition and the role of initial pushouts for the applicability of productions we refer to [EEPT06, MEE11]. 3 M -Functor from Petri Net to Graph Transformation Systems In this section we recall on the one hand the M -adhesive category (PTINet,M1) of Petri nets with individual tokens (together with the class M1 of all injective morphisms), on the other hand, we consider the well-known M -adhesive category (AGraphsATG,M2) of typed attributed graphs (together with the class M2 of all injective morphisms with isomorphism on the data type part) with a suitable attributed Petri net type graph ATG = PNTG shown in Figure 2 with data type signature Σ−nat and algebra TΣ−nat ∼= NAT for rules and graphs. Note that we use the term algebra TΣ−nat without variables. Moreover, we explain by example the construction of the restricted M -functor F : PTINet|M1 → AGraphsPNTG|M2 between both categories (see [MEE11]), which is only defined on injective morphisms M1. We construct the functor between the categories restricted to M -morphisms, but this is not an M -functor F : (PTINet,M1) → (AGraphsPNTG, M2) because F is not well-defined on non-injective morphisms (see counterex- ample in [MEE11], where the constructed typed attributed graph morphism does not preserve attributes in and wpre). On the other hand, the restriction to injective Petri net morphisms for match and rule morphisms makes sense in view of preserving the firing behavior. This implies that we need only a very restrictive version of morphisms for typed attributed graphs, namely M2-morphisms, to simulate and create Petri net transformations using rules without variables. Definition 3 (Category PTINet [MGH11]) • Objects in PTINet are Petri nets with individual tokens (PTI nets) defined by NI = (N,I,m), where N = (P,T, pre, post) is a classical place/transition net, I is a set of individual tokens and m : I → P a marking function assigning a place m(x)∈ P to each x ∈ I. • PTINet-morphisms are given by a triple of functions f = ( fP : P1 → P2, fT : T1 → T2, fI : I1 → I2) : NI1 → NI2 s.t. the following diagrams commute with pre and post, respectively. T1 = P1⊕ T2 P2⊕ pre1 post1 fT fP ⊕ pre2 post2 I1 = P1 I2 P2 m1 fI fP m2 Proc. PNGT 2012 4 / 12 ECEASST Place Token Trans in : nat out : nat place2trans weightpre : nat trans2 place weightpost : nat token2place Figure 2: Attributed type graph PNTG The notion of attributed graphs combined with the typing concept leads to the well-known cat- egory of typed attributed graphs AGraphsATG, where attributed graphs are typed over an at- tributed type graph ATG [EEPT06]. Here, we con- sider a specific type graph PNTG (see [MEE11]) to express PTI nets as graphs, which is shown in Figure 2. The meaning of every depicted element of PNTG is as follows: The nodes Place, Trans, and Token represent the elements of PTI nets that can be depicted as nodes in typed attributed graphs and hence give the possible node typing. The edges place2trans and trans2 place have the attributes weightpre and weightpost which give weights for edges in pre- and postdomain of transitions in the corresponding PTI net. Node Trans has two attributes in and out that encode the number of places in the pre- and postdo- main of a transition (to ensure the preservation of a transition node’s environment using graph morphisms). All node and edge attributes are typed over natural numbers. a b p1 t1 p2 2 1 a : Token b : Token p1 : Place t1 : Trans in = 1 out = 1 p2 : Place (a, p1) : token2 place (b, p1) : token2 place (p1,t1) : place2trans weightpre = 2 (t1, p1) : trans2 place weightpost = 1 Figure 3: Applying functor F to a PTI net In [MEE11] the functor F : PTINet|M1 → AGraphsPNTG|M2 translating PTI nets into typed attributed graphs is formally defined. An ex- ample for using the functor on objects is shown in Figure 3, where the typed attributed graph on the right side is the translation of the cor- responding PTI net on the left side. Intu- itively, the translation works as follows: Indi- vidual tokens, places, and transitions are trans- lated into the nodes of the corresponding types Token, Place, and Trans. Edges between individ- ual tokens, places, and transitions are translated into the graph edges of the corresponding types token2place,trans2place,place2trans. Weights of the edges between places and transitions are trans- lated into the weightpre and weightpost attributes of the corresponding graph edges. Finally, the number of places in the pre- and postdomain of a transition is recorded as values of the in and out attributes of the transition node. Although we do not have an M -functor F : (PTINet,M1) → (AGraphsPNTG, M2), it is shown in [MEE11] that we can apply the theory of Section 2, especially Theorem 1, to the restricted M -functor F : PTINet|M1 → AGraphsPNTG|M2 constructed above. In fact, it is suf- ficient to verify the following adapted properties, which are shown in [MEE11], to apply the theory to transformations with injective matches in M1 resp. M2: F translates pushouts of M1-morphisms in (PTINet,M1) into pushouts of M2-morphisms in (AGraphsPNTG,M2), F creates M1-morphisms and F preserves initial pushouts over M1-morphisms. Hence, according to [MEE11], we know already that F translates and creates rule appli- cability, construction of (direct) transformations with injective matches as well as parallel and sequential independence of transformations. 5 / 12 Volume 51 (2012) Transfer of Local Confluence and Termination between PN and GT Systems 4 F -Transfer of Local Confluence In this section, we consider under which conditions local confluence can be translated by M - functor F : (C1,M1)→(C2,M2) from one transformation system AS1 = (C1,M1,P) to another one AS2 = (C2,M2,F (P)) with translated productions F (P) and, vice versa, under which con- ditions local confluence of AS1 can be created by F from local confluence of AS2. According to [EEPT06], an M -adhesive transformation system (C,M ,P) is locally conflu- ent, if for all direct transformations G ⇒ H1 and G ⇒ H2 there is an object X together with transformations H1 ∗⇒ X and H2 ∗⇒ X . In the case of confluence this property is required for transformations G ∗⇒ H1 and G ∗⇒ H2. Theorem 2 (Translation and Creation of Local Confluence) Let AS1 = (C1,M1,P), AS2 = (C2,M2,F (P)) be M -adhesive transformation systems and F : (C1,M1)→ (C2,M2) be an M -functor that translates and creates (direct) transformations as well as creates morphisms (see Theorem 1). Then AS1 is locally confluent for all transforma- tion spans H1 ρ1,m1⇐= G ρ2,m2 =⇒ H2 iff AS2 is locally confluent for all translated transformation spans F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2). Proof. 1. (Translation): Assume local confluence of H1 ρ1,m1⇐= G ρ2,m2 =⇒ H2 in AS1. Then there exist an object X and transformations H1 ∗⇒ X, H2 ∗⇒ X via P. Due to the assumption that F translates (direct) transformations, there exist the object X′ = F (X) and transformations F (H1) ∗⇒ F (X), F (H2) ∗⇒ F (X) via F (P). Hence, the translated transformation span F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2) is locally confluent in AS2. 2. (Creation): Assume local confluence of F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2) in AS2. Then there is an object X′ and transformations F (H1) ∗⇒ X′, F (H2) ∗⇒ X′ via F (P). Due to the assumption that F creates (direct) transformations, there exist objects X1, X2 and transformations H1 ∗⇒ X1, H2 ∗⇒ X2 via P with F (X1) ∼= X′ ∼= F (X2). Hence, F (X1) ∼= F (X2) and the assumption that F creates morphisms and hence also isomor- phisms implies that X1 ∼= X2. We get that H1 ρ1,m1⇐= G ρ2,m2 =⇒ H2 is locally confluent in AS1. A well-known approach for the verification of local confluence is the analysis of critical pairs. A critical pair P1 ρ1,o1⇐= K ρ2,o2 =⇒ P2 is a pair of parallel dependent transformations with a minimal overlapping K of the left sides of the rules. Definition 4 (F -Reachable Critical Pair) Given an M -functor F : (C1,M1) → (C2,M2). An F -reachable critical pair of productions F (ρ1) and F (ρ2) is a critical pair in AS2 of the form F (R1) F (K1) F (L1) F (L2) F (K2) F (R2) F (P1) F (N1) F (K) F (N2) F (P2) F (o1) F (o2) F (l1)F (r1) F (v1)F (w1) F (l2) F (r2) F (w2)F (v2) Proc. PNGT 2012 6 / 12 ECEASST where all morphisms of type F (A)→F (B) are of the form F ( f ) for some morphism f : A→B. In the following, we assume that F is compatible with pair factorization, where pair factor- ization intuitively means that for every pair of objects there is a smallest overlapping embedded into a given context (see [EEPT06]). For details concerning compatibility with pair factorization see also Definition 6 in [MEE12]. Another important well-known result that we use in our approach is the lemma Completeness of Critical Pairs [EEPT06]. This lemma states that for each pair of parallel dependent direct transformations, we have a critical pair that can be embedded into the given parallel dependent transformation span. Furthermore, we use the Local Confluence Theorem [EEPT06] to analyze whether a given M -adhesive transformation system is locally confluent. This is the case, if all critical pairs P1 ρ1,o1⇐= K ρ2,o2 =⇒ P2 of the given transformation system are strictly confluent. Strictness means in- tuitively that the largest substructure of K that is preserved by the critical pair is also preserved by the merging transformation steps P1 ∗⇒ K′ and P2 ∗⇒ K′ (see the diagram to the right). K P1 P2 K′ ρ1,o1 ρ2,o2 ∗ ∗ The following proposition describes in which case a pair of translated transformations is lo- cally confluent. The detailed proof of Proposition 1 is given in [MEE12]. It is based on the fact that for each translated pair of parallel dependent transformations, we can construct the corre- sponding embedded F -reachable critical pair, which is by assumption strictly confluent. Proposition 1 (Local Confluence of a Translated Transformation Span) Given M -adhesive transformation systems AS1 = (C1,M1,P), AS2 = (C2, M2, F (P)) and an M -functor F : (C1,M1)→ (C2,M2) that creates (direct) transformations and morphisms (see Theorem 1) and is compatible with pair factorization. Then, a translated transformation span F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2) is locally confluent if all F -reachable critical pairs of F (ρ1) and F (ρ2) in AS2 are strictly confluent. Now we summarize the results concerning the creation of local confluence based on F - reachable critical pairs. Theorem 3 (Creation of Local Confluence Based on F -Reachable Critical Pairs) Given an M -functor F : (C1,M1) → (C2,M2) with the assumptions of Proposition 1. An M - adhesive transformation system AS1 is locally confluent for all transformation spans H1 ρ1,m1⇐= G ρ2,m2 =⇒ H2 if all F -reachable critical pairs of F (ρ1) and F (ρ2) in AS2 are strictly confluent. Proof. The strict confluence of all F -reachable critical pairs of F (ρ1) and F (ρ2) implies that AS2 is locally confluent for all translated transformation spans F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2) by Proposition 1. This implies the local confluence of AS1 for all transformation spans H1 ρ1,m1⇐= G ρ2,m2 =⇒ H2 by Theorem 2. 7 / 12 Volume 51 (2012) Transfer of Local Confluence and Termination between PN and GT Systems Application to Petri Net and Graph Transformation Systems The functor F : PTINet|M1 → AGraphsPNTG|M2 described in Section 3 is compatible with pair factorization, and hence satisfies the requirements of Theorem 3 (see Proposition 2 in [MEE12]), such that we have creation of local confluence based on critical pairs. Hence, by application of Theorem 3, a PTI net transformation system (N,P) with a PTI net N and a set of productions P is locally confluent, if all F -reachable critical pairs of corresponding graph rules F (ρ1) and F (ρ2) are strictly confluent with ρ1,ρ2 ∈ P. Example 1 (Mobile Dining Philosophers) Let us consider a slight extension of the well-known Dining Philosophers model, where mobile philosophers now may also leave or join a table ( MoDiPhi). The firing of the PTI net transitions models the traditional behavior of the philosophers, switching between thinking and eating (see the PTI net in the left part of Figure 4 modelling five philosophers sitting at one table). The additional structural changes of the net occurring when a philosopher joins or leaves a ta- ble are modelled by the set PMoDiPhi = {JoinTable,LeaveTable} of PTI net transformation rules. The right part of Figure 4 shows the PTI net transformation rule JoinTable for reconfiguring the table when another philosopher joins it1. The second transformation rule LeaveTable (not shown) is inverse to rule JoinTable, i.e., left-hand and right-hand sides are interchanged. The dia- ea1 t1 th1 t′1 lf1 ea2 t2 th2 t′2 lf2 ea3 t3 th3 t′3 lf3 ea4 t4 th4 t′4 lf4 ea5 t5 th5 t′5 lf5 e f c h i ga d b j Ginit lfj eaj tj thj t′j lfk t ′′ i thi x z L1 thi eaj thj lfj lfk x z I1 lfj eaj tj thj t′j lfi eai ti thi t′i lfk x y z R1 l1 r1 Figure 4: PTI net (left) and PTI net rule JoinTable (right) of transformation system MoDiPhi gram in Figure 5 shows the strict confluence of the F -reachable critical pair of the F -translated graph rules (F (JoinTable),F (JoinTable))2. The spans F (P1) F (w1)←− F (N1) F (v1)−→ F (K) and F (K) F (v2)←− F (N2) F (w2)−→ F (P2) in the upper half of the diagram denote the two conflicting rule applications of the rule F (JoinTable), where one rule application deletes the two transitions that are used by the other rule application and creates new ones. Graph F (N) in the center is the largest substructure of F (K) that is preserved by the critical pair. In the lower half of the dia- gram, we can see how the two direct graph transformations F (K)⇒F (P1) and F (K)⇒F (P2) can be merged again by applying once more the rule F (JoinTable) at an adequate match to the graphs F (P1) and F (P2). Moreover, the strictness condition is satisfied because F (N) is also preserved by the merging transformations F (P1)⇒ F (K′′) and F (P2)⇒ F (K′′). As we can show strict confluence also for all other F -reachable critical pairs of our example, 1 Note that the token inscriptions x,y,z are not variables but identifiers indicating the rule morphisms. 2 A screenshot of the AGG analysis tool showing this critical pair can be found in [MEE12], Figure 6. Proc. PNGT 2012 8 / 12 ECEASST we obtain by Theorem 3 that the PTI net transformation system MoDiPhi is locally confluent. lf1 :Place ea1 :Place t1 :Trans in=3 out=1 th1 :Place t′1 :Trans in=1 out=3 lf4 :Place ea4 :Place t4 :Trans in=3 out=1 th4 :Place t′4 :Trans in=1 out=3 lf2 :Place t′′5 :Trans in=1 out=1 th5 :Place d:Token a:Token b:Token c:Token F(P1) th4 :Place lf2 :Place ea1 :Place th1 :Place lf1 :Place t′′5 :Trans in=1 out=1 th5 :Place d:Token a:Token c:Token F(N1) lf1 :Place ea1 :Place t1 :Trans in=3 out=1 th1 :Place t′1 :Trans in=1 out=3 lf2 :Place t′′4 :Trans in=1 out=1 th4 :Place a:Token t′′5 :Trans in=1 out=1 th5 :Place d:Token c:Token F(K) th5 :Place lf2 :Place ea1 :Place th1 :Place lf1 :Place t′′4 :Trans in=1 out=1 th4 :Place a:Token d:Token c:Token F(N2) lf1 :Place ea1 :Place t1 :Trans in=3 out=1 th1 :Place t′1 :Trans in=1 out=3 lf5 :Place ea5 :Place t5 :Trans in=3 out=1 th5 :Place t′5 :Trans in=1 out=3 lf2 :Place t′′4 :Trans in=1 out=1 th4 :Place a:Token d:Token b:Token c:Token F(P2) lf1 :Place ea1 :Place t1 :Trans in=3 out=1 th1 :Place t′1 :Trans in=1 out=3 lf5 :Place b′:Token lf2 :Place th4 :Place th5 :Place ea5 :Place a:Token d:Tokenc:Token F(N4) lf1 :Place ea1 :Place t1 :Trans in=3 out=1 th1 :Place t′1 :Trans in=1 out=3 lf5 :Place ea5 :Place t5 :Trans in=3 out=1 th5 :Place t′5 :Trans in=1 out=3 lf4 :Place ea4 :Place t4 :Trans in=3 out=1 th4 :Place t′4 :Trans in=1 out=3 lf2 :Place a:Token b:Tokenb′:Token c:Token d:Token F(K′′) lf4 :Place ea4 :Place t4 :Trans in=3 out=1 th4 :Place t′4 :Trans in=1 out=3 lf2 :Place a:Token b:Token c:Token ea1 :Place th1 :Place lf1 :Place th5 :Place d:Token F(N3) lf2 :Place th4 :Place th5 :Place ea1 :Place lf1 :Place th1 :Place a:Tokenc:Token d:Token F(N) F(w1) F(v1) F(w2) F(v2) F(z1) F(z2) ∃F(z4)∃F(z3) F(v4) F(w4) F(v3) F(w3) (PB) (2) (=) (3) (=) (4) (=) Figure 5: Strict confluence of the F -reachable critical pair of the F -translated graph rules (F (JoinTable),F (JoinTable)) 5 F -Transfer of Termination and Functional Behavior A transformation G ∗⇒ H is called terminating if no production is applicable to H anymore. A formal definition of termination of an M -adhesive transformation system is as follows. Definition 5 (Termination and F -Termination of an M -Adhesive Transformation System) • An M -adhesive transformation system (C1,M1,P) is called terminating if there is no infi- nite sequence G0 ρ1,m1 =⇒ G1 ρ2,m2 =⇒ G2 ρ3,m3 =⇒ ... with ρ1,ρ2,ρ3,...∈P and matches m1,m2,m3,... • Given an M -functor F : (C1,M1)→ (C2,M2), a translated M -adhesive transformation system (C2,M2,F (P)) is called F -terminating if there is no infinite sequence F (G0) F (ρ1),m′1 =⇒ G′1 F (ρ2),m′2 =⇒ G′2 F (ρ3),m′3 =⇒ ... with F (ρ1),F (ρ2),F (ρ3),... ∈ F (P) and matches m′1,m ′ 2,m ′ 3,... 9 / 12 Volume 51 (2012) Transfer of Local Confluence and Termination between PN and GT Systems M -functors transfer termination according to the following theorem. Theorem 4 (F -Transfer of Termination) Given M -adhesive transformation systems AS1 = (C1,M1,P), AS2 = (C2, M2, F (P)) and an M -functor F : (C1,M1) → (C2,M2) that translates and creates (direct) transformations (see Theorem 1). Then, an M -adhesive transformation system AS1 is terminating iff the correspond- ing translated M -adhesive transformation system AS2 is F -terminating. Proof. By contraposition: Given a nonterminating sequence in AS2 (see diagram to the right). It is possible to generate stepwise a nonterminating sequence in AS1 by application of the assumption that the given M -functor creates direct transformations. Analogously, given a nonterminating se- quence in AS1, it is possible to generate stepwise a nonter- minating sequence in AS2 by application of the assumption that the given M -functor translates direct transformations. G0 G1 G2 ... F (G0) G′1= F (G1) G′2= F (G2) ... F F F ρ1,m1 ρ2,m2 ρ3,m3 F (ρ1),m′1 = F (m1) F (ρ2),m′2 = F (m2) F (ρ3),m′3 = F (m3) According to [EEPT06] a locally confluent and terminating transformation system AS is con- fluent and has functional behavior in the following sense: For each object G there is an object H together with a terminating transformation G ∗⇒ H in AS and H is unique up to isomorphism. Moreover, each pair of transformations G ∗⇒ H1 and G ∗⇒ H2 can be extended to terminating transformations G ∗⇒ H1 ∗⇒ H and G ∗⇒ H2 ∗⇒ H with the same object H. Corollary 1 (F -Transfer of Local Confluence, Termination and Functional Behavior) Let F : (C1,M1) → (C2,M2) be an M -functor between M -adhesive transformation systems AS1 and AS2 with the assumptions of Theorem 2. AS1 is locally confluent and terminating iff AS2 is locally confluent and F -terminating. Moreover, AS1 has functional behavior if AS2 is locally confluent and F -terminating. Proof. This follows directly from Theorem 2, Theorem 4 and [EEPT06]. Application to Petri Net and Graph Transformation Systems The functor F : PTINet|M1 → AGraphsPNTG|M2 described in Section 3 satisfies already the assumptions of Theorem 4 and Corollary 1. Hence, by application of Theorem 4 and Corol- lary 1, we have F -transfer of local confluence, termination and functional behavior. Moreover, Theorem 3 allows us to create local confluence of a Petri net transformation system by critical pair analysis of the corresponding graph transformation system. Example 2 Our MoDiPhi PTI net transformation system with rule set PMoDiPhi = {JoinTable,LeaveTable} (see Example 1) is obviously not terminating because the two rules are inverse to each other. Considering a restricted rule set containing only rule LeaveTable, the transformation system becomes terminating because rule LeaveTable reduces the size (number of places, transitions and Proc. PNGT 2012 10 / 12 ECEASST tokens) of the PTI net it is applied to with each rule application. Constructing the F -translated rule F (LeaveTable), we obviously get an F -terminating graph transformation system, because also F (LeaveTable) reduces the size of the graph it is applied to with each rule application. 6 Related Work and Conclusion In our previous paper [MEE11] we have developed a general framework to establish a formal relationship between different M -adhesive transformation systems. In Section 2 of the present paper we have reviewed the main result of [MEE11] showing under which conditions transforma- tions can be translated and created between different M -adhesive transformation systems. This result is based on suitable properties of M -functors between the corresponding M -adhesive cat- egories. Especially we have constructed in [MEE11] and reviewed in Section 3 an M -functor from Petri nets with individual tokens to typed attributed graphs, which is restricted to M - morphisms and satisfies the adapted properties given at the end of Section 3. As main new results of this paper we have extended this framework to the transfer of local confluence, termi- nation and functional behavior. This allows us to use the critical pair analysis of the AGG-tool for typed attributed graphs to analyze Petri net transformation systems. Furthermore, we have pointed out in Section 4 that the concrete restricted M -functor constructed in [MEE11] fulfills the additional property (the compatibility of F with pair factorization), so that the main results from Section 4 and Section 5 can be applied. On this basis, a straightforward extension is to consider also firing steps as transformation rules in AGraphsPNTG, and to analyze dependencies and conflicts between net transformations and firing steps using AGG. In future work we will analyze how nested application conditions [HP05, EHL+10] can be handled in this framework in order to transfer critical pairs and local confluence of M -adhesive transformation systems with nested application conditions. Furthermore, the restricted M -functor from Petri nets with individual tokens to typed at- tributed graphs can be considered to become an equivalence of categories between Petri nets with individual tokens and a suitable subcategory of typed attributed graphs. In future work we will analyze, whether it is easier to verify the required properties for the corresponding inclu- sion functor than for the original restricted M -functor. Moreover, we will apply the general framework also to other M -adhesive transformation systems. References [AGG09] TFS-Group, TU Berlin. AGG. 2009. http://tfs.cs.tu-berlin.de/agg. [BEHM07] E. Biermann, C. Ermel, F. Hermann, T. Modica. A Visual Editor for Reconfigurable Object Nets based on the ECLIPSE Graphical Editor Framework. In Proc. Workshop on Algorithms and Tools for Petri Nets (AWPN’07). 2007. [EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. EATCS Monographs in Theor. Comp. Science. Springer, 2006. 11 / 12 Volume 51 (2012) http://tfs.cs.tu-berlin.de/agg Transfer of Local Confluence and Termination between PN and GT Systems [EGH10] H. Ehrig, U. Golas, F. Hermann. Categorical Frameworks for Graph Transformation and HLR Systems based on the DPO Approach. Bulletin of the EATCS 102:111– 121, 2010. [EHL+10] H. Ehrig, A. Habel, L. Lambers, F. Orejas, U. Golas. Local Confluence for Rules with Nested Application Conditions. In Ehrig et al. (eds.), Proceedings of Intern. Conf. on Graph Transformation. LNCS 6372, pp. 330–345. Springer, 2010. [EHP+08] H. Ehrig, K. Hoffmann, J. Padberg, C. Ermel, U. Prange, E. Biermann, T. Modica. Petri Net Transformations. In Petri Net Theory and Applications. Pp. 1–16. I-Tech Education and Publication, 2008. [HM10] K. Hoffmann, T. Modica. Formal Modeling of Communication Platforms using Re- configurable Algebraic High-Level Nets. ECEASST 30:1–25, 2010. [HP05] A. Habel, K.-H. Pennemann. Nested constraints and application conditions for high- level structures. In Kreowski et al. (eds.), Formal Methods in Software and Systems Modeling. LNCS 3393, pp. 294–308. Springer, 2005. [LS04] S. Lack, P. Sobociński. Adhesive Categories. In Proc. FOSSACS’ 04. LNCS 2987, pp. 273–288. Springer, 2004. [MEE11] M. Maximova, H. Ehrig, C. Ermel. Functors between M -adhesive Categories Ap- plied to Petri Net and Graph Transformation Systems. In Ermel and Hoffmann (eds.), Proc. Int. Workshop on Petri Nets and Graph Transformation Systems. Vol- ume 40. ECEASST, 2011. [MEE12] M. Maximova, H. Ehrig, C. Ermel. Transfer of Local Confluence and Termination between Petri Net and Graph Transformation Systems Based on M -Functors: Ex- tended Version. Technical report 2012/08, TU Berlin, 2012. http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2012 [MGH11] T. Modica, K. Gabriel, K. Hoffmann. Transformation of Petri Nets with Individual Tokens. ECEASST 40, 2011. [PEH07] J. Padberg, H. Ehrig, K. Hoffmann. Formal Modeling and Analysis of flexible Pro- cesses in Mobile Ad-Hoc Networks. Bulletin of the EATCS 91:128–132, 2007. [PEHP08] U. Prange, H. Ehrig, K. Hoffman, J. Padberg. Transformations in Reconfig- urable Place/Transition Systems. In Concurrency, Graphs and Models. LNCS 5065, pp. 96–113. Springer, 2008. [RON07] TFS-Group, TU Berlin. Reconfigurable Object Nets Environment. 2007. http://www.tfs.cs.tu-berlin.de/roneditor Proc. PNGT 2012 12 / 12 http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2012 http://www.tfs.cs.tu-berlin.de/roneditor Introduction Basic Concepts M-Functor from Petri Net to Graph Transformation Systems F-Transfer of Local Confluence F-Transfer of Termination and Functional Behavior Related Work and Conclusion