Formal Relationship between Petri Net and Graph Transformation Systems based on Functors between M-adhesive Categories Electronic Communications of the EASST Volume 40 (2011) Proceedings of the 4th International Workshop on Petri Nets and Graph Transformation (PNGT 2010) Formal Relationship between Petri Net and Graph Transformation Systems based on Functors between M -adhesive Categories Maria Maximova, Hartmut Ehrig and Claudia Ermel 18 pages Guest Editors: Claudia Ermel, 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 Formal Relationship between Petri Net and Graph Transformation Systems based on Functors between M -adhesive Categories 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: Various kinds of graph transformations and Petri net transformation sys- tems are examples of M -adhesive transformation systems based on M -adhesive categories, generalizing weak adhesive HLR categories. For typed attributed graph transformation systems, the tool environment AGG allows the modeling, the simu- lation and the analysis of graph transformations. A corresponding tool for Petri net transformation systems, the RON-Environment, has recently been developed which implements and simulates Petri net transformations based on corresponding graph transformations using AGG. Up to now, the correspondence between Petri net and graph transformations is handled on an informal level. The purpose of this paper is to establish a formal relationship between the corresponding M -adhesive transfor- mation systems, which allow the translation of Petri net transformations into graph transformations with equivalent behavior, and, vice versa, the creation of Petri net transformations from graph transformations. Since this is supposed to work for dif- ferent kinds of Petri nets, we propose to define suitable functors, called M -functors, between different M -adhesive categories and to investigate properties allowing us the translation and creation of transformations of the corresponding M -adhesive transformation systems. Keywords: M -adhesive transformation system, equivalence, graph transformation, Petri net transformation, M -adhesive category 1 Introduction Modeling the adaptation of a dynamic system to a changing environment gets more and more im- portant. Application areas cover e.g. computer supported cooperative work, multi agent systems or mobile networks. One approach to combine formal modeling of dynamic systems and con- trolled model adaption are reconfigurable Petri nets. The main idea is the stepwise development of place/transition nets by applying net transformation rules [EHP+08, PEHP08]. This approach increases the expressiveness of Petri nets and allows in addition to the well known token game a formal description and analysis of structural changes. Rule-based Petri net transformation is related to graph transformation [EEPT06]. For typed attributed graph transformation systems, the well-established tool AGG [AGG09] allows the modeling, the simulation and the analysis of graph transformations. Recently, a tool for recon- figurable Petri nets, called RON-Tool [TFS07, BEHM07] (Reconfigurable Object Nets), exe- 1 / 18 Volume 40 (2011) mailto:mascham@cs.tu-berlin.de mailto:ehrig@cs.tu-berlin.de mailto:claudia.ermel@tu-berlin.de Translation and Creation of Transformations cutes and analyzes Petri net transformations based on corresponding graph transformations us- ing AGG. As a matter of fact, the correspondence between Petri net and graph transformations is handled on an informal level up to now. Since both graph and net transformation systems are formally defined, the aim of this paper is to propose formal criteria ensuring a semantical correspondence of reconfigurable Petri nets and their corresponding representations as graph transformation systems. An M -adhesive transformation system is a general categorical transformation framework based on M -adhesive categories, which rely on a class M of monomorphisms, generalizing weak adhesive HLR categories. The double-pushout approach, based on categorical construc- tions, is a suitable description of transformations leading to results like the Local Church-Rosser, Parallelism, Concurrency, Embedding, Extension, and Local Confluence Theorems [EEPT06]. A set of rules over an M -adhesive category according to the double-pushout approach consti- tutes an M -adhesive transformation system [EGH10]. Aiming for a more general approach to ensure a semantical correspondence of different trans- formation systems, we establish a formal relationship between two corresponding M -adhesive transformation systems. This correspondence allows us especially the translation of Petri net transformations into graph transformations and, vice versa, the creation of Petri net transforma- tions from graph transformations in order to analyze the behavior of Petri net transformation systems by analyzing their translation in terms of typed attributed graph transformation sys- tems using the tool AGG [AGG09]. We propose to define suitable functors, called M -functors, between different M -adhesive categories and to investigate properties, which allow us the trans- lation and creation of transformations of the corresponding M -adhesive transformation systems. The paper is structured as follows: Section 3 introduces the formal notions M -adhesive trans- formation systems and M -functors. The first main result given in Section 4 states that an M - functor translates rules in a way that applicablility and transformation results are translated as well. Vice versa, the second main result states that an M -functor also creates applicability of rules in the other direction. Section 5 applies these new main result to the translation and creation of Petri net transformations by constructing and analyzing an M -functor from the category of place/transition nets to the category of typed attributed graphs with corresponding type graph1. In Section 6, we conclude and propose interesting future research directions. 2 Related Work In [MM90], Meseguer and Montanari represented Petri nets as graphs equipped with operations for composition of transitions. They introduced categories for Petri nets with and without initial markings and functors expressing duality and invariants. Their constructions provide a formal basis for expressing concurrency in terms of algebraic structures over graphs and categories. Based on categorical Petri nets, in [DS02], Petri nets are related to automata with concurrency relations by establishing a correspondence as coreflection between the associated categories. A first approach to relate Petri nets and graph transformation systems has been proposed by Kre- owski in [Kre81], where Petri net firing behavior is expressed by graph transformation rules. In our approach, we want to consider Petri net transformations in addition. Moreover, we aim for a 1 For the results in Section 5, we give only proof ideas. More detailed proofs are given in [MEE11]. Proc. PNGT 2010 2 / 18 ECEASST more general approach that establishes a semantical correspondence not only between Petri net and graph transformation systems but between any kind of formally defined rule-based transfor- mation systems that can be generalized as M -adhesive transformation systems. In order to transform not only graphs, but also high-level structures as Petri nets and alge- braic specifications, high-level replacement (HLR) categories were established in [EHKP91a, EHKP91b], which require a list of so-called HLR properties to hold. They were based on a morphism class M used for the rule morphisms. This framework allowed a rich theory of trans- formations for all HLR categories, but the HLR properties were difficult and lengthy to verify for each category. Combining adhesive categories [LS04] and HLR categories lead to (weak) adhesive HLR categories in [EHPP06] and to M -adhesive categories in [EGH10], where a sub- class M of monomorphisms is considered and only pushouts over M -morphisms have to fulfill the van Kampen property (a certain compatibility of pushouts and pullbacks). Not only many kinds of graphs, but also different kinds of place/transition nets and algebraic high-level nets are M -adhesive and also weak adhesive HLR categories which allows the application of the theory to all these kinds of structures [EEPT06, PE07, MGE+09]. In fact, all results in [EEPT06] for weak adhesive HLR categories are also valid for M -adhesive categories [EGH10]. 3 M -Adhesive Categories, Transformation Systems and M -Functors An M -adhesive category [EGH10], consists of a category C together with a class M of monomor- phisms as defined in Definition 1 below. The concept of M -adhesive categories generalises that of weak adhesive, adhesive HLR and adhesive categories [LS04]. The category of typed at- tributes graphs and several categories of Petri nets are weak adhesive HLR (see [EEPT06]) and hence also M -adhesive. Definition 1 (M -Adhesive Category) An M -adhesive category (C,M ) is a category C together with a class M of monomorphisms satisfying • C has pushouts (POs) and pullbacks (PBs) along M -morphisms, • M is closed under composition, decomposition, POs and PBs, • POs along M -morphisms are M -VK-squares, 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. A B C D A′ B′ C′ D′ m f g n m′ f ′ g′n ′ a b c d Definition 2 (M -Adhesive Transformation System and Independence) Given an M -adhesive category (C,M ). • An M -adhesive transformation system AS = (C,M ,P) has in addition a set P of produc- tions of the form ρ = (L l←− K r−→ R) with l,r ∈ M . 3 / 18 Volume 40 (2011) Translation and Creation of Transformations A direct transformation G ρ,m =⇒ H via production ρ and match m consists of two POs (1) and (2) as shown in the diagram to the right, where n : R → H is called comatch of m. A production ρ is applicable via m to G, if we have a PO complement D in (1), such that (1) becomes a PO. L K R G D H (1) (2) l r m n • Two (direct) transformations G ρ1,m1 =⇒ H1 and G ρ2,m2 =⇒ H2 are called parallel independent, if there are morphisms d12 : L1 → D2, d21 : L2 → D1 such that l∗1 ◦d21 = m2 and l∗2 ◦d12 = m1. Dually G ρ1,m1 =⇒ H1 and H1 ρ2,m2 =⇒ H2 are sequentially independent if H1 ρ1 −1,n1 =⇒ G and H1 ρ2,m2 =⇒ H2 are parallel independent, where ρ1−1 = (R1 r1←−K1 l1−→ L1) and n1 is the comatch of m1. R1 K1 L1 L2 K2 R2 H1 D1 G D2 H2 m1 d12 m2 d21 l1 l∗1 l2 l∗2 In order to study translation and creation of transformations between different M -adhesive transformation systems we introduce the notion of an M -functor. An M -functor establishes a semantical correspondence between different M -adhesive transformation systems. Definition 3 (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. On purpose we don’t require that an M -functor preserves pullbacks along M -morphisms, VK-squares, or other properties, but later additional properties of F will be required in order to achieve specific results. Remark 1 If we want to consider only (direct) transformations with injective matches, as in the case of Petri net transformations in the next section, then it is sufficient to define the functor F on injective morphisms only. Moreover, this restriction is necessary, if F is not well-defined for non-injective morphisms. For this case we need to define a special kind of an M -functor: a restricted M -functor. Definition 4 (Restricted M -Functor) A functor F : C1|M1 → C2|M2 between M -adhesive categories (C1,M1) and (C2,M2) with Ci|Mi the restriction of Ci to Mi-morphisms for i = 1,2 is called a restricted M -functor, if F (M1) ⊆ M2 and F translates POs along M1-morphisms in (C1,M1) into POs along M2- morphisms in (C2,M2). Proc. PNGT 2010 4 / 18 ECEASST 4 Translation and Creation of Transformations To obtain a semantical correspondence between any two transformation systems we need to en- sure that the respective transformation systems together with their relevant properties are trans- lated and reflected properly. Given an M -adhesive transformation system AS1 = (C1,M1,P1) with an M -adhesive cat- egory (C1,M1) and productions P1. We want to translate transformations from AS1 to AS2 = (C2,M2,P2) with M -adhesive category (C2,M2) and suitable productions P2. This can be done using an M -functor F : (C1,M1)→ (C2,M2) for P2 = F (P1). Theorem 1 (Translation of Transformations) An M -functor F : (C1,M1) → (C2,M2) translates applicability of productions, construction of (direct) transformations , as well as parallel and sequential independence of transformations. Proof. AS2 = (C2,M2,F (P1)) is a well-defined M -adhesive transformation system, because F trans- lates M1-morphisms into M2-morphisms for the productions and each direct transformation G ρ,m =⇒ H in AS1 given by pushouts (1) and (2) leads to a direct transformation F (G) F (ρ),F (m) =⇒ F (H) in AS2 given by pushouts (3) and (4), because F preserves pushouts along M -morphisms. L K R G D H (1) (2) l r m ⇒ F (L) F (K) F (R) F (G) F (D) F (H) (3) (4) F (l) F (r) F (m) Moreover, the functor property of F implies that F translates parallel and sequential indepen- dence of transformations. As shown above, we need for translation of transformations from AS1 to AS2 only the basic properties of an M -functor. This is no longer true for creation of transformations in AS1 from transformations in AS2 with P2 = F (P1) as above. Definition 5 (Creation of Applicability and Direct Transformations) 1. An M -functor F : (C1,M1)→ (C2,M2) creates applicability of a production ρ = (L l←− K r−→ R) to object G, if applicability of F (ρ) to F (G) with match m′ : F (L) → F (G) implies applicability of ρ to G with some match m : L → G and F (m) = m′. 2. 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: 5 / 18 Volume 40 (2011) Translation and Creation of Transformations F (L) F (K) F (R) F (G) D′ H′ (1) (2) F (l) F (r) m′ ⇒ L K R G D H (3) (4) l r m 3. F creates parallel (and similarly sequential) independence, if parallel independence of F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2) in AS2 implies parallel independence of H1 ρ1,m1⇐= G ρ2,m2 =⇒ H2 in AS1. Remark 2 If F creates parallel (sequential) independence, then F characterises parallel (sequential) in- dependence, i.e., parallel (sequential) independence in AS1 is equivalent to parallel (sequential) independence in AS2, because F already preserves parallel (sequential) independence by Theo- rem 1. In the following we formulate the properties for an M -functor F , such that we have cre- ation of applicability, direct transformations and parallel (sequential) independence. But first we review the notion of initial pushouts motivated by Remark 3 below. Definition 6 (Initial Pushout) Given a morphism f : G → G′ in an M -adhesive category (C,M ). (1) is an initial pushout (IPO) over f with boundary B, context C and b,c ∈ M , if (1) is PO ∧∀ POs (2) over f (defined by the outer diagram) with h,h′ ∈ M =⇒ ∃!b∗ : B → B′,c∗ : C →C′. h◦b∗ = b ∧ h′◦c∗ = c ∧ (3) is a PO. B G B′ (2) C G′ C′ (1)(3) = = b b∗ k h c c∗ k′ h′ f Remark 3 For each match m : L → G with initial pushout (4) and b ∈ M1, a production ρ = (L l←−K r−→R) is applicable with match m : L→G, iff the following “gluing condition” is satisfied: there is b′ : B → K in M1 with l ◦b′ = b. In this case the pushout complement D in (5) can be constructed as pushout of b′ ∈ M1 and a leading to h : C → D,k : K → D and an induced morphism d : D → G, s.t., (5) is pushout and (7) commutes (see [EEPT06]). B L K C G D (4) (5) (6) (7) b l a b′ h k d m Definition 7 (Properties of M -Functors) 1. An M -functor F : (C1,M1)→(C2,M2) creates morphisms, if for all m′ : F (L)→F (G) in (C2,M2) there is exactly one morphism m : L → G with F (m) = m′. 2. F preserves initial pushouts, if for each initial pushout (IPO) (1) over m : L → G, also (2) is initial pushout over F (m) : F (L)→ F (G). Proc. PNGT 2010 6 / 18 ECEASST B (1) L C G b m ⇒IPO in (C1,M1) IPO in (C2,M2) F (B) (2) F (L) F (C) F (G) F (b) F (m) This leads to the following theorem on creation of transformations by M -functors: Theorem 2 (Creation of Transformations) Given an M -functor F : (C1,M1)→(C2,M2) with initial pushouts in (C1,M1), which creates morphisms and preserves initial pushouts, then F creates applicability of productions, direct transformations, as well as parallel and sequential independence of transformations. Proof. 1. F creates applicability of productions Given ρ = (L l←− K r−→ R) and match m′ : F (L)→F (G), s.t., F (ρ) is applicable to m′. Since F creates morphisms we have a unique m : L → G with F (m) = m′. Let (1) be an initial pushout over m in the diagram below. By assumption on F , (2) is initial pushout over F (m) and (4),(5) are POs. This means, that F (ρ) is applicable to m′ = F (m). According to Remark 3, this implies the existence of b′′ : F (B)→ F (K) in M2 with F (l)◦b′′ = F (b). L K RB C G D H (3) (6)(1) l r m b′ a b ⇐ F (L) F (K) F (R)F (B) F (C) F (G) D′ H′ (4) (5)(2) F (l) F (r) m′ b′′ F (b) F (a) Since F creates morphisms there is a unique morphism b′ : B → K with F (b′) = b′′. More- over, uniqueness of creation of morphisms implies l◦b′ = b and hence b′∈M1 by decomposition property of M1. Hence the gluing condition is satisfied and we have applicability of ρ to G with match m : L → G and F (m) = m′ with pushout complement D in (3). 2. F creates direct transformations Given the direct transformation F (G) F (ρ),m′ =⇒ H′ in AS2 by pushouts (4) and (5) in (C2,M2). We have already constructed pushout (3) in (C1,M1) and can construct pushout (6) along r ∈ M1 leading to a direct transformation G ρ,m =⇒ H. Since F preserves pushouts along M - morphisms and pushout complements in (C2,M2) and they are unique up to isomorphism. We have F (D)∼= D′, F (H)∼= H′ and hence also F (G) F (ρ),F (m) =⇒ F (H) in AS2. 3. F creates parallel (sequential) independence By parallel independence of F (H1) F (ρ1),F (m1)⇐= F (G) F (ρ2),F (m2) =⇒ F (H2) in AS2 we have mor- 7 / 18 Volume 40 (2011) Translation and Creation of Transformations phisms d′12 : F (L1) → F (D2) with F (l ∗ 2)◦d′12 = F (m1) and d ′ 21 : F (L2) → F (D1) with F (l∗1)◦d′21 = F (m2) leading to corresponding morphisms d12 : L1 → D2 and d21 : L2 → D1 with l∗2 ◦d12 = m1 and l∗1 ◦d21 = m2, because F creates morphisms uniquely and preserves composition. Remark 4 For the case described in the Remark 1 we have to show for Theorem 1 that F translates pushouts of M1-morphisms in (C1,M1) into pushouts of M2-morphisms in (C2,M2). For Theorem 2 we need in addition, that F creates M -morphisms, i.e., for each (m′ : F (L) → F (G)) ∈ M2 there is exactly one morphism (m : L → G) ∈ M1 with F (m) = m′ and F pre- serves initial pushouts over M1-morphisms. Note, that we cannot replace the M -adhesive cate- gories (Ci,Mi) for i = 1,2 by (Ci|Mi,Mi), because (Ci|Mi,Mi) are in general not M -adhesive. 5 Translation and Creation of Petri Net Transformations According to our overall aim in Section 1 we want to construct a functor from Petri nets to typed attributed graphs and show how to apply the main results of Theorem 1 and Theorem 2 in order to translate and create Petri net transformations using graph transformations. For this purpose we review on one hand the M -adhesive categories (PTINet,M1) of Petri nets with individual tokens and class M1 of all injective morphisms, which is defined and shown to be M -adhesive in [MGE+09]. On the other hand we review typed attributed graphs (AGraphsATG,M2), which are shown to be M -adhesive in [EEPT06] and we define a suitable attributed Petri net type graph AT G = PNT G. Moreover we construct a functor F between both categories, which, however, is only defined on injective morphisms M1. Note, that we do not use Petri nets with “classical initial markings”, known as Petri net systems [Rei85], because the corresponding M -adhesive category requires a class M leading to Petri net rules which are marking preserving. Marking preserving rules are not adequate to model firing steps as direct transformations since tokens must not be created or deleted. Other choices for (C1,M1) would be Petri nets without initial marking or algebraic high-level nets (see [EEPT06, Rei85, MGE+09]). In fact, we can construct a functor F : PTINet|M1 → AGraphsPNTG|M2 between the cate- gories restricted to M -morphisms, but not an M -functor F : (PTINet,M1)→ (AGraphsPNTG, M2), because F is not well-defined on non-injective morphisms (see counterexample in Figure 1 below, where F ( f ) does not preserve attributes in and wpre). This means, we proceed as dis- cussed in Remark 4, which allows the application of Theorem 1 and Theorem 2 in order to obtain translation and creation of Petri net transformations with injective morphisms. For application of Theorem 1 we need steps 1.-5., and for Theorem 2 in addition steps 6. and 7. 1. Definition of Petri nets with individual Tokens: PTINet. 2. Definition of typed attributed graphs over Petri net type graph PNT G: AGraphsPNTG. 3. Translation of PTI nets into PNT G-typed attributed graphs (definition of functor F on objects). 4. Translation of restricted PTINet-morphisms into restricted AGraphsPNTG-morphisms (def- inition of functor F : PTINet|M1 → AGraphsPNTG|M2 on morphisms). Proc. PNGT 2010 8 / 18 ECEASST 5. F translates pushouts of M1-morphisms in (PTINet,M1) into pushouts of M2-morphisms in (AGraphsPNTG,M2). 6. F creates M1-morphisms. 7. F preserves initial pushouts over M1-morphisms. Figure 1: Counterexample for general (non-injective) morphisms 5.1 Petri Nets with Individual Tokens: PTINet For classical place / transition (P/T) nets N we adopt the approach of Meseguer and Montanari [MM90] using free commutative monoids P⊕ over P, where N = (P,T, pre, post) with places P, transitions T , functions pre, post : T → P⊕ and markings M ∈ P⊕. Petri nets NI = (P,T, pre, post,I,m) with individual tokens are place/transition nets N = (P,T, pre, post) together with a set I of individual tokens and a marking function m : I →P assigning a place m(x) ∈ P to each x ∈ I. Therefore two (or more) different individual tokens x,y ∈ I may be on the same place, i.e. m(x) = m(y), while in the standard “collective token approach” the marking M ∈ P⊕ tells us only how many tokens we have on each place, but we are not able to distinguish between two tokens on the same place. A formal definition of a Petri net with individual tokens is as follows ([MGE+09]). Definition 8 (Petri Net with Individual Tokens) A Petri net with individual tokens NI = (P,T, pre, post,I,m) is given by a classical P/T net N = (P,T, pre : T → P⊕, post : T → P⊕), where P⊕ is the free commutative monoid over P, a (possibly infinite) set of individual tokens I, and the marking function m : I → P, assigning to each individual token x ∈ I the corresponding place m(x)∈ P. PTINet-morphisms now define not only a mapping between two P/T nets but also between their individual tokens: Definition 9 (PTINet-Morphism) A PTINet-morphism f : NI1 → NI2 is given by a triple of functions f = ( fP : P1 → P2, fT : T1 → T2, fI : I1 → I2), such that the following diagrams commute with pre and post respectively. 9 / 18 Volume 40 (2011) Translation and Creation of Transformations T1 = P1⊕ T2 P2⊕ pre1 post1 fT fP ⊕ pre2 post2 I1 = P1 I2 P2 m1 fI fP m2 It is also shown in [MGE+09], that (PTINet,M1) with the class M1 of all injective morphisms is an M -adhesive category, where pushouts and pullbacks are constructed componentwise (see Figure 2, where (1) is an example for a pushout in (PTINet,M1), with individual tokens colored in black). Figure 2: PO in PTINet In the following we only consider the restriction of PTINet to M1-morphisms, PTINet|M1 , in order to define the functor F in Subsection 5.4, because F is not well-defined on general mor- phisms. But we use the M -adhesive category (PTINet,M1) in order to define pushouts, because (PTINet|M1,M1) is not M1-adhesive due to the well-known fact, that the induced morphism of M1-morphisms is in general not an M1-morphism. 5.2 Typed Atributed Graphs over Petri Net Type Graph PNTG According to [EEPT06] the category (AGraphsATG,M2) of typed attributed graphs with class M2 of all injective morphisms with isomorphism on the data type part is M -adhesive, where pushouts along M2-morphisms are constructed componentwise in the graph part. Proc. PNGT 2010 10 / 18 ECEASST Place Token Trans nat token2 place place2trans trans2place weightpost weightpre in out Place Token Trans in : nat out : nat place2trans weightpre : nat trans2 place weightpost : nat token2 place Σ−nat sorts : nat opns : z :→ nat succ : nat → nat NAT NATnat = N znat = 0 ∈N succnat : N→N x 7→ x + 1 Figure 3: Type graph PNTG with data type signature Σ−nat and algebra NAT Objects in AGraphs are pairs (G,D) of an E-Graph G with sig- nature E (shown to the right), and Σ−nat data type D, where in the following we only use D = TΣ−nat ∼= NAT . This means, G is given by G = (V GG ,V G D = N,E G G ,E G NA,E G EA,(s G j ,t G j ) j∈{G,NA,EA} ), where V GG resp. V G D are the graph resp.-data nodes of G, E G G , E G NA, EG VG ENA VD EEA sG tG sNA tNA sEA tEA resp. E GEA are the graph edges resp. node attribute and edge attribute edges of G and s G j ,t G j are corresponding source and target functions for the edges. In our case, the type graph ATG is the Petri net type graph PNTG shown in Figure 3 with data type signature Σ−nat and algebra TΣ−nat ∼= NAT for rules and graphs, where the E-Graph of PNTG is shown on the left and its attribute notation on the right of Figure 3. Objects in AGraphsPNTG are pairs (AN,type) with attributed graph AN = (G,D) with D = NAT and AGraphs-morphism type : (G,D)→(PNTG,Dfin) with final Σ−nat data type Dfin. Morphisms in AGraphsPNTG are defined componentwise and are type compatible with morphisms in AGraphs. Four sample morphisms in AGraphsPNTG are shown in Figure 4, where a pushout is constructed. 5.3 Translation of PTI Nets into PNTG-typed Attributed Graphs A formal definition of the functor F on objects is given as follows. Definition 10 (Translation of PTINet-Objects) Given a PTI net NI = (P,T, pre, post,I,m). We define the object F (NI) = ((G,NAT ),type) in AGraphsPNTG with type : (G,NAT )→ (PNT G,D f in) and G = (V GG ,V G D = N,E G G ,E G NA,E G EA, (sGj ,t G j ) j∈{G,NA,EA} ) as follows, where we use the following abbreviations: token2place , to2 p, place2trans , p2t,trans2 place , t2 p,weightpre , wpre,weightpost , wpost and pre(t)(p) = nP ∈ N for pre(t) = ∑p∈P nP · p ∈ P⊕ and similar for post(t)(p). 11 / 18 Volume 40 (2011) Translation and Creation of Transformations Figure 4: PO in AGraphsPNTG V GG = P]T ]I E GG = E G to2 p ]E G p2t ]E G t2 p with E Gto2 p ={(x, p)∈ I ×P | m(x) = p}, E G p2t ={(p,t)∈ P×T | pre(t)(p) > 0} and E Gt2 p ={(t, p)∈ T ×P | post(t)(p) > 0} E GNA = E G in ]E G out with E Gin ={(t,n,in) | (t,n)∈ T ×N∧|•t|= n}, E Gout ={(t,n,out) | (t,n)∈ T ×N∧|t •|= n}, where •t and t• are the pre- and post-domains of t ∈ T with cardinalities |•t| and |t •|. E GEA = E G wpre ]E G wpost with E Gwpre = { (p,t,n)∈ E Gp2t ×N | pre(t)(p) = n } E Gwpost = { (t, p,n)∈ E Gt2p ×N | post(t)(p) = n } sGG,t G G : E G G →V G G defined by s G G(a,b) = a resp. t G G (a,b) = b sGNA : E G NA →V G G , t G NA : E G NA →N defined by s G NA(t,n,x) = t resp. t G NA(t,n,x) = n sGEA : E G EA → E G G defined by s G EA(p,t,n) = (p,t) and s G EA(t, p,n) = (t, p) t GEA : E G EA →N defined by t G EA(p,t,n) = n and t G EA(t, p,n) = n Proc. PNGT 2010 12 / 18 ECEASST The corresponding type-morphism is given in Definition 11 below. An example for using the functor F on objects is shown in Figure 4, where the four typed attributed graphs are translations of the corresponding four PTI nets in Figure 2. Definition 11 (AGraphsPNTG-Morphism type) The AGraphsPNTG-morphism type : (G,NAT ) → (PNT G,D f in) is given by final morphism of data types and typeG : G → PNT G given by E-graph morphism typeG = (typeVG,typeVD,typeEG, typeENA,typeEEA) where typeVG : V G G →V PNT G G with x 7→ Place (x ∈ P), x 7→ Trans (x ∈ T ), x 7→ Token (x ∈ I) typeVD : N→ D f innat with x 7→ nat (x ∈N) typeEG : E G G → E PNT G G with x 7→ y for x ∈ E G y and y ∈{to2p, p2t,t2 p} typeENA : E G NA → E PNT G NA with x 7→ y for x ∈ E G y and y ∈{in,out} typeEEA : E G EA → E PNT G EA with x 7→ y for x ∈ E G y and y ∈{wpre,wpost} 5.4 Translation of Restricted PTINet-Morphisms into Restricted AGraphsPNTG-Morphisms We now define the functor F : PTINet|M1 → AGraphsPNTG|M2 on injective morphisms. A counterexample for the translation of non-injective morphisms is given in Figure 1, examples for injective morphisms in Figure 2 and corresponding translated morphisms in Figure 4. Definition 12 (Translation of PTINet-Morphisms) For each PTINet-morphism f : NI1 → NI2 with f = ( fP, fT , fI) ∈ M1, i.e. fP, fT , fI injective, we define F ( f ) : F (NI1)→ F (NI2) where F (NIi) = (ViG,N,EiG,EiNA,EiEA,(si j,ti j) j∈{G,NA,EA}) with i = 1,2 by F ( f ) = f ′ = ( f ′VG, f ′ VD, f ′ EG, f ′ ENA, f ′ EEA) with f ′VG : V1G →V2G with ViG = Pi ]Ti ]Ii for i = 1,2 by f ′ VG = fP ] fT ] fI f ′VD : N→N by f ′ VD = idN f ′EG : E1G → E2G with EiG = Eito2 p ]Ei p2t ]Eit2 p by f ′EG(x, p) = ( fI(x), fP(p)) for (x, p)∈ E1to2 p f ′EG(p,t) = ( fP(p), fT (t)) for (p,t)∈ E1 p2t f ′EG(t, p) = ( fT (t), fP(p)) for (t, p)∈ E1t2 p f ′ENA : E1NA → E2NA with EiNA = Eiin ]Eiout by f ′ENA(t,n,i) = ( fT (t),n,i) for (t,n,i)∈ E1in ]E1out ∧i ∈{in,out} f ′EEA : E1EA → E2EA with EiEA = Eiwpre ]Eiwpost by f ′EEA(p,t,n) = ( fP(p), fT (t),n) for (p,t,n)∈ E1wpre f ′EEA(t, p,n) = ( fT (t), fP(p),n) for (t, p,n)∈ E1wpost 13 / 18 Volume 40 (2011) Translation and Creation of Transformations Lemma 1 (Well-Definedness of Morphism Translation) For each f : NI1 → NI2 in PTINet with f ∈ M1 is F ( f ) : F (NI1)→ F (NI2) in AGraphsPNTG well-defined with F ( f )∈ M2. Moreover F preserves inclusions. Proof. A detailed proof is given in [MEE11] showing the following steps: 1. f ′VG, f ′ VD, f ′ EG, f ′ ENA, f ′ EEA are well-defined w.r.t. codomain. 2. The components of F ( f ) are compatible with sources and targets. 3. The components of F ( f ) are compatible with typing morphisms. 4. f ∈ M1 (inclusion) implies F ( f )∈ M2 (inclusion). 5.5 Translation of Pushouts We have to show, that if (1) is a PO in PTINet with fi ∈ M1, then we have that (2) is a PO in AGraphsPNTG with F ( fi)∈ M2. NI0 (1) NI1 NI2 NI3 f1 f2 f4 f3 F (NI0) (2) F (NI1) F (NI2) F (NI3) F ( f1) F ( f2) F ( f4) F ( f3) Since POs in PTINet are constructed componentwise, we know that the P-, T - and I-components of (1) are POs in Sets. Since also POs in AGraphsATG and AGraphsPNTG are constructed com- ponentwise we have to show that the VG-, VD-, EG-, ENA- and EEA-components of (2) are POs in Sets. This is clear for the VG-components fiVG = fiP] fiT ] fiI , because POs are compatible with coproducts and for fiD, because all components are identities. For the EG-component we have to show, that (3) is PO in Sets, which follows if (4) and similar (4a) resp. (4b) with “to2p” and “ fiI × fiP” replaced by “p2t” and “ fiP × fiT ” resp. “t2p” and “ fiT × fiP” are POs. E0G (3) E1G E2G E3G F ( f1)G F ( f2)G F ( f4)G F ( f3)G E0to2 p (4) E1to2 p E2to2 p E3to2 p f1I × f1P f2I × f2P f4I × f4P f3I × f3P For the ENA- and EEA components, it is sufficient to show POs (5) and (6) and similar (5a) with “in” replaced by “out” and (6a) with “pre” replaced by “post”. E0in (5) E1in E2in E3in f1T ×idN f2T ×idN f4T ×idN f3T ×idN E0wpre (6) E1wpre E2wpre E3wpre f1P × f1T f2P × f2T f4P × f4T f3P × f3T Proc. PNGT 2010 14 / 18 ECEASST All these diagrams commute, because each product component commutes by assumption. But it is more difficult to show explicitly, that they are POs (see for example Lemma 2 below), because products of POs are in general not POs. An example is the translation of the PO in PTINet shown in Figure 2 to the PO in AGraphsPNTG shown in Figure 4. Lemma 2 (Translation of Pushouts) Diagrams (4) and (4a) are pushouts. Proof. See [MEE11]. 5.6 Creation of Injective Morphisms Given F (NI1),F (NI2) and f ′ : F (NI1)→ F (NI2)∈ M2 with type compatible morphisms f ′VG : V1G →V2G with ViG = Pi ]Ti ]Ii for i = 1,2 f ′VD : N→N with f ′ VD = idN f ′EG : E1G → E2G with EiG = Eito2 p ]Ei p2t ]Eit2 p f ′ENA : E1NA → E2NA with EiNA = Eiin ]Eiout f ′EEA : E1EA → E2EA with EiEA = Eiwpre ]Eiwpost Define f : NI1 → NI2 with NI j = (Pj,Tj, pre j, post j,I j,m j) for j = 1,2 by f = ( fP : P1 → P2, fT : T1 → T2, fI : I1 → I2) with fT (t) = f ′ VG(t) for t ∈ T1 ⊆V1G fP(p) = f ′ VG(p) for p ∈ P1 ⊆V1G fI(x) = f ′ VG(x) for x ∈ I1 ⊆V1G Well-definedness of f : NI1 → NI2 ∈ M1 follows from Lemma 3 below, where the proof of part 2 is based on Lemma 4. The proofs of both Lemma are given in [MEE11]. Lemma 3 (Well-Definedness of Creation of Injective Morphisms) Given the construction above for f : NI1 → NI2. The following holds: 1. f ′VG(t)∈ T2, f ′ VG(p)∈ P2, f ′ VG(x)∈ I2, and 2. squares (1),(2) to the right commute with injec- tive fP, fT , fI . T1 (1) P1⊕ T2 P2⊕ pre1 post1 fT fP ⊕ pre2 post2 I1 (2) P1 I2 P2 m1 fI fP m2 Lemma 4 (PTI-Morphism-Lemma) f : NI1 → NI2 is an injective PTINet-morphism ⇔ f = ( fP, fT , fI) is injective with 1−4, where 1. ∀t ∈ T1.p ∈•t ⇔ fP(p)∈• fT (t) and ∀t ∈ T1.p ∈ t•⇔ fP(p)∈ fT (t)• 2. ∀(p,t)∈ P1 ⊗T1 = E1 p2t. (p,t,n)∈ E1wpre ⇔ ( fP(p), fT (t),n)∈ E2wpre and ∀(t, p)∈ T1 ⊗P1 = E1t2 p. (t, p,n)∈ E1wpost ⇔ ( fT (t), fP(p),n)∈ E2wpost 15 / 18 Volume 40 (2011) Translation and Creation of Transformations 3. ∀t ∈ T1. card(•t) = n ⇔ card(• fT (t)) = n and card(t•) = n ⇔ card( fT (t)•) = n with •t ={p ∈ P1 | pre1(t)(p) > 0} and t•={p ∈ P1 | post1(t)(p) > 0} 4. ∀x ∈ I1.(x, p)∈ E1to2 p ⇔ ( fI(x), fP(p))∈ E2to2 p 5.7 Preservation of Initial Pushouts The proof of this property is based on the initial PO constructions for PTINet in [MGE+09] and for AGraphsATG in [EEPT06]. Details of the proof are given in [MEE11]. An example is given in Figure 5, where (1) is an initial PO over f in PTINet, (2) the induced PO over F ( f ), and the initial PO over F ( f ) in AGraphsPNTG is given by the outer diagram with corners B′,C′,F (L),F (G). Since i′ and j′ are isomorphisms, diagram (2) is already initial PO over F ( f ). Figure 5: Preservation of Initial Pushouts 6 Conclusion and Future Work As pointed out already in Section 1 we want to develop a general framework to establish a for- mal relationship between different M -adhesive transformation systems based on M -adhesive categories. The main idea is to construct a suitable M -functor between the corresponding M - adhesive categories, which translates pushouts, creates morphisms and preserves initial pushouts. Proc. PNGT 2010 16 / 18 ECEASST This allows by Theorem 1 and Theorem 2 the translation and creation of transformations between the corresponding M -adhesive transformation systems, including parallel and sequential inde- pendence of transformations. Moreover, we have discussed the restriction to injective matches via M1-morphisms, which requires only a functor for M1-morphisms. In Section 5 we have discussed a corresponding functor from Petri nets with individual tokens to typed attributed graphs. We have verified that this functor translates pushouts of M1-morphisms, creates M1-morphisms and preserves initial pushouts over M1-morphisms, which allows the ap- plication of Theorem 1 and Theorem 2 in connection with Remark 4. In future work, we will provide sufficient conditions in order to ensure that the M−functor preserves initial pushouts2. In the long run, this should allow the analysis of interesting prop- erties of Petri net transformation systems, like termination and local confluence in addition to parallel and sequential independence, using corresponding results and analysis tools like AGG for graph transformation systems. Moreover, it is interesting to study the relationship between other M -adhesive transformation systems using this approach, e.g. high-level Petri nets and typed attributed graphs as well as triple graphs and flattening of triple graphs. Acknowledgements: Some of the authors are partly supported by the German Research Coun- cil project Behaviour Simulation and Equivalence of Systems Modelled by Graph Transformation (Behaviour-GT). 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. Work- shop on Algorithms and Tools for Petri Nets (AWPN’07). 2007. http://tfs.cs.tu-berlin.de/publikationen/Papers07/BEHM07.pdf [DS02] M. Droste, R. M. Shortt. From Petri Nets to Automata with Concurrency. Applied Categorical Structures 10:173–191, 2002. 10.1023/A:1014305610452. http://dx.doi.org/10.1023/A:1014305610452 [EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. EATCS Monographs in Theor. Comp. Science. Springer, 2006. [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. http://tfs.cs.tu-berlin.de/publikationen/Papers10/EGH10.pdf [EHKP91a] H. Ehrig, A. Habel, H.-J. Kreowski, F. Parisi-Presicce. From Graph Grammars to high level replacement systems. In 4th Int. Workshop on Graph Grammars and their Application to Computer Science. LNCS 532, pp. 269–291. Springer, 1991. 2 First steps in this direction are Lemma 5 and Lemma 6 in [MEE11]. 17 / 18 Volume 40 (2011) http://tfs.cs.tu-berlin.de/agg http://tfs.cs.tu-berlin.de/publikationen/Papers07/BEHM07.pdf http://dx.doi.org/10.1023/A:1014305610452 http://tfs.cs.tu-berlin.de/publikationen/Papers10/EGH10.pdf Translation and Creation of Transformations [EHKP91b] H. Ehrig, A. Habel, H.-J. Kreowski, F. Parisi-Presicce. Parallelism and Concurrency in High-Level Replacement Systems. Math. Struct. in Comp. Science 1:361–404, 1991. [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. [EHPP06] H. Ehrig, A. Habel, J. Padberg, U. Prange. Adhesive High-Level Replacement Sys- tems: A New Categorical Framework for Graph Transformation. Fundamenta In- formaticae 74(1):1–29, 2006. [Kre81] H.-J. Kreowski. A Comparison between Petri Nets and Graph Grammars. In 5th International Workshop on Graph-Theoretic Concepts in Computer Science. LNCS 100, pp. 1–19. Springer, 1981. [LS04] S. Lack, P. Sobociński. Adhesive Categories. In Proc. FOSSACS 2004. 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. Technical report 2011/04, TU Berlin, 2011. http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2011 [MGE+09] T. Modica, K. Gabriel, H. Ehrig, K. Hoffmann, S. Shareef, C. Ermel, U. Golas, F. Hermann, E. Biermann. Low- and High-Level Petri Nets with Individual Tokens. Technical report 2009/13, Technische Universität Berlin, 2009. http://www.eecs. tu-berlin.de/menue/forschung/forschungsberichte/2009. [MM90] J. Meseguer, U. Montanari. Petri Nets are Monoids. Information and Computation 88(2):105–155, 1990. [PE07] U. Prange, H. Ehrig. From Algebraic Graph Transformation to Adhesive HLR Categories and Systems. In Algebraic Informatics. Proceedings of CAI 2007. LNCS 4728, pp. 122–146. Springer, 2007. [PEHP08] U. Prange, H. Ehrig, K. Hoffman, J. Padberg. Transformations in Reconfigurable Place/Transition Systems. In Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday. LNCS 5065, pp. 96–113. Springer, 2008. [Rei85] W. Reisig. Petri Nets: An Introduction. EATCS Monographs on Theoretical Com- puter Science 4. Springer, 1985. [TFS07] TFS-Group, TU Berlin. Reconfigurable Object Nets Environment. 2007. http://www.tfs.cs.tu-berlin.de/roneditor Proc. PNGT 2010 18 / 18 http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2011 http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2009 http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2009 http://www.tfs.cs.tu-berlin.de/roneditor Introduction Related Work M-Adhesive Categories, Transformation Systems and M-Functors Translation and Creation of Transformations Translation and Creation of Petri Net Transformations Petri Nets with Individual Tokens: PTINet Typed Atributed Graphs over Petri Net Type Graph PNTG Translation of PTI Nets into PNTG-typed Attributed Graphs Translation of Restricted PTINet-Morphisms into Restricted AGraphsPNTG-Morphisms Translation of Pushouts Creation of Injective Morphisms Preservation of Initial Pushouts Conclusion and Future Work