paper.dvi Electronic Communications of the EASST Volume 2 (2006) Proceedings of the Workshop on Petri Nets and Graph Transformation (PNGT 2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories Ulrike Prange 13 pages Guest Editors: Paolo Baldan, Hartmut Ehrig, Julia Padberg, Grzegorz Rozenberg Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 ECEASST Algebraic High-Level Nets as Weak Adhesive HLR Categories Ulrike Prange Department of Software Engineering and Theoretical Computer Science Technical University of Berlin, Germany uprange@cs.tu-berlin.de Abstract: Adhesive high-level replacement (HLR) systems have been recently introduced as a new categorical framework for double pushout transformations. Al- gebraic high-level nets combine algebraic specifications with Petri nets to allow the modelling of data, data flow and data changes within the net. In this paper, we show that algebraic high-level schemas and nets fit well into the context of weak adhesive HLR categories. This allows us to apply the developed theory also to algebraic high-level net transformations. Keywords: Algebraic High-Level Nets, Adhesive HLR Categories 1 Introduction Adhesive high-level replacement (HLR) systems have been recently introduced as a new cate- gorical framework for graph transformation in the double pushout approach [EHPP06, EEPT06]. They combine the well-known framework of HLR systems with the framework of adhesive cate- gories introduced by Lack and Sobociński [LS05]. The main concept behind adhesive categories are the so-called van Kampen squares, which ensure that pushouts along monomorphisms are stable under pullbacks and, vice versa, that pullbacks are stable under combined pushouts and pullbacks. In the case of adhesive HLR categories the class of all monomorphisms is replaced by a subclass M of monomorphisms closed under composition and decomposition. Algebraic high-level (AHL) nets combine algebraic specifications with Petri nets [PER95] to allow the modelling of data, data flow and data changes within the net. In general, an AHL net denotes a net based on a specification SP in combination with an SP-algebra A, in contrast a net without a specific algebra is called a schema. While many types of graphs and graph-like structures are adhesive HLR categories, the cate- gories of elementary nets, place/transition nets as well as AHL schemas with fixed specification only satisfy a weaker version of adhesive HLR categories [EP06] called weak adhesive HLR categories. The reason is that the category PTNets of place/transition nets has general pullbacks, but pullbacks in general cannot be constructed componentwise in Sets. However, pullbacks along monomorphisms in PTNets can be constructed componentwise in Sets. This is the key idea to weaken the concept of adhesive HLR categories using weak VK squares. In this case, van Kampen squares ensure the corresponding properties only under stricter requirements on the morphisms. Nevertheless, the framework of weak adhesive HLR categories is still sufficient to show under some additional assumptions (which are necessary also in the non-weak case) as 1 / 13 Volume 2 (2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories main results the Local Church-Rosser Theorem, the Parallelism Theorem, the Concurrency The- orem, the Embedding and Extension Theorem and the Local Confluence Theorem, also called Critical Pair Lemma. Thus, underlying an adhesive HLR systems we consider either a weak or a non-weak adhesive HLR category. Since this concept of adhesive HLR systems includes all kinds of graphs mentioned above, and also elementary nets, place/transition nets and AHL schemas with fixed specification, adhesive HLR systems can be seen as a suitable unifying framework for graph and Petri net transforma- tions. The question arises, if and how different types of AHL schemas and nets, where we do not fix the algebra or the specification, fit into the framework of adhesive HLR systems. In case of AHL nets with fixed specification SP, this category of AHL nets can be shown to be a weak adhesive HLR category, if the underlying category of algebras Algs(SP), together with a suitable morphism class M , is a weak adhesive HLR category. Generalized AHL schemas, where the specification may change, can be shown to be a weak adhesive HLR category using an isomorphic comma category construction. In case both specification and algebra may change, the corresponding category of generalized AHL nets is a weak adhesive HLR category, if the category of all algebras can be shown to be a weak adhesive HLR category. These three results are the main new contributions of this paper. This paper is organized as follows: In Section 2, we introduce weak adhesive HLR categories and systems and review in Section 3, that different kinds of Petri nets are weak adhesive HLR categories. In Section 4, AHL schemas and nets are described and shown to be weak adhesive HLR categories. In Section 5, we present generalized AHL schemas and nets and prove the properties of a weak adhesive HLR category. At last, in Section 6 we give a conclusion and identify future work. 2 Review of Weak Adhesive HLR Categories and Systems The intuitive idea of (weak) adhesive HLR categories are categories with suitable pushouts and pullbacks which are compatible with each other. More precisely the definition is based on so- called van Kampen squares. The idea of a van Kampen (VK) square is that of a pushout which is stable under pullbacks, and vice versa that pullbacks are stable under combined pushouts and pullbacks. Definition 1 A pushout (1) is a van Kampen square, if for any commutative cube (2) with (1) in the bottom and the back faces being pullbacks holds: the top face is a pushout if and only if the front faces are pullbacks. A′ B′ A B C′ D′ C D (2) m′ a f ′ g′ b m f n′ c d n g A B C D (1) m f n g Since not even in the category Sets of sets and functions each pushout is a van Kampen square, Proc. PNGT 2006 2 / 13 ECEASST for (weak) adhesive HLR categories only those VK squares of Definition 1 are considered where m is a monomorphism. The main difference between (weak) adhesive HLR categories as described in [EHPP06, EEPT06] and adhesive categories introduced in [LS05] is that a distinguished class M of monomorphisms is considered instead of all monomorphisms, so that only pushouts along M - morphisms have to be VK squares. In the weak case, only special cubes are considered for the VK square property. Definition 2 A category C with a morphism class M is a (weak) adhesive HLR category, if 1. M is a class of monomorphisms closed under isomorphisms, composition ( f : A → B ∈ M , g : B →C ∈ M ⇒ g◦ f ∈ M ) and decomposition (g◦ f ∈ M , g ∈ M ⇒ f ∈ M ), 2. C has pushouts and pullbacks along M -morphisms and M -morphisms are closed under pushouts and pullbacks, 3. pushouts in C along M -morphisms are (weak) VK squares. For a weak VK square, the VK square property holds for all commutative cubes with m ∈ M and ( f ∈ M or b, c, d ∈ M ) (see Definition 1). The categories Sets of sets and functions, Graphs of graphs and graph morphisms and GraphsTG of typed graphs and typed graph morphisms are adhesive HLR categories for the class M of all monomorphisms. Moreover, an important example is the category (AGraphsATG, M ) of typed attributed graphs with a type graph AT G and the class M of all injective morphisms with isomorphisms on the data part. The categories ElemNets of elementary nets and PTNets of place/transition nets with the class M of all corresponding monomorphisms fail to be adhesive HLR categories, but they are weak adhesive HLR categories (see Section 3). Both adhesive and weak adhesive HLR categories are closed under product, slice, coslice, functor and comma category constructions. That means we can construct new (weak) adhesive HLR categories from given ones. Theorem 1 If (C, M1) and (D, M2) are (weak) adhesive HLR categories, then the following categories are also (weak) adhesive HLR categories: 1. the product category (C×D, M1×M2), 2. the slice category (C\X , M1 ∩C\X ) and the coslice category (X\C, M1 ∩X\C) for any object X in C, 3. for every category X the functor category ([X, C], M1-functor transformations), where an M1-functor transformation is a natural transformation t : F → G where all morphisms tX : F(X ) → G(X ) are in M1, 4. the comma category (ComCat(F, G; I ), M ) with M = (M1 ×M2)∩MorComCat(F,G;I ) and functors F : C → X, G : D → X, where F preserves pushouts along M1-morphisms and G preserves pullbacks (along M2-morphisms). 3 / 13 Volume 2 (2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories Now we are able to generalize graph transformation systems, grammars and languages in the sense of [Ehr79, EEPT06]. In general, an adhesive HLR system is based on productions, also called rules, that describe in an abstract way how objects in this system can be transformed. An application of a production is called a direct transformation and describes how an object is actually changed by the production. A sequence of these applications yields a transformation. Definition 3 Given a (weak) adhesive HLR category (C, M ), a production p = (L l ← K r → R) (also called rule) consists of three objects L, K and R called left hand side, gluing object and right hand side respectively, and morphisms l : K → L, r : K → R with l, r ∈ M . Given a production p = (L l ← K r → R) and an object G with a morphism m : L → G, called match, a direct transformation G p,m =⇒H from G to an object H is given by the following diagram, where (1) and (2) are pushouts. A sequence G0 ⇒ G1 ⇒ ... ⇒ Gn of direct transformations is called a transformation and is denoted as G0 ∗ ⇒ Gn. L K R G D H (1) (2) l r m k n f g An adhesive HLR system AH S = (C, M , P) consists of a (weak) adhesive HLR category (C, M ) and a set of productions P. 3 Petri Nets as Weak Adhesive HLR Categories Petri net transformation systems have been first introduced in [EHKP91] for the case of low-level nets and in [PER95] for high-level nets using the algebraic presentation of Petri nets as monoids introduced in [MM90]. The main idea of Petri net transformation systems is to extend the well- known theory of Petri nets based on the token game by general techniques which allow to change also the structure of the nets. In [Pad96], a systematic study of Petri net transformation systems has been presented in the categorical framework of abstract Petri nets, which can be instantiated to different kinds of low-level and high-level Petri nets. In this section we introduce our notion of elementary nets and place/transition nets and re- capitulate that the respective categories (ElemNets, M ) and (PTNets, M ) are weak adhesive HLR categories (see [EP06]). The corresponding instantiations of adhesive HLR systems lead to different kinds of Petri net transformation systems. Definition 4 An elementary net is given by N = (P, T, pre, post) with a set P of places, T of transitions, and pre- and post-domain functions pre, post : T → P(P), where P is the power set functor. An elementary net morphism f : N → N′ is given by f = ( fP : P →P ′, fT : T → T ′) compatible with the pre- and post-domain functions, i.e. pre′◦ fT = P( fP)◦ pre and post ′◦ fT = P( fP)◦ post. Elementary nets and elementary net morphisms form the category ElemNets. Proc. PNGT 2006 4 / 13 ECEASST Corollary 1 The category (ElemNets, M ) is a weak adhesive HLR category, where M is the class of all injective morphisms. Proof Idea. The category ElemNets is isomorphic to the comma category ComCat(IDSets, P; I ), where P : Sets → Sets is the power set functor and I = {1, 2}. Ac- cording to Theorem 1.4 it suffices to note that (Sets, M ) is a weak adhesive HLR category and that P : Sets → Sets preserves pullbacks along injective morphisms. Note, that (ElemNets, M ) is not an adhesive HLR category as stated in [EEPT06], since P only preserves pullbacks along injective morphisms, but not over general ones. Definition 5 A place/transition net N = (P, T, pre, post) is given by a set P of places, a set T of transitions, as well as pre- and post-domain functions pre, post : T → P⊕, where P⊕ is the free commutative monoid over P. A place/transition net morphism f : N → N′ is given by f = ( fP : P→ P ′, fT : T →T ′) compat- ible with the pre- and post-domain functions, i.e. pre′◦ fT = f ⊕ P ◦ pre and post ′◦ fT = f ⊕ P ◦ post. Place/transition nets and place/transition net morphisms form the category PTNets. Corollary 2 The category (PTNets, M ) is a weak adhesive HLR category, if M is the class of all injective morphisms. Proof Idea. The category PTNets is isomorphic to the comma category ComCat(IDSets, � ⊕; I ) with I = {1, 2}, where �⊕ : Sets → Sets is the free commutative monoid functor. According to Theorem 1.4 it suffices to note that (Sets, M ) is a weak adhesive HLR category and that �⊕ : Sets → Sets preserves pullbacks along injective morphisms. The following example shows that (PTNets, M ) is not an adhesive HLR category. This is due to the fact, that �⊕ : Sets → Sets does not preserve general pullbacks. This would imply that pullbacks in PTNets are constructed componentwise for places and transitions. Example 1 In Figure 1, the square (1) with non-injective morphisms g1, g2, p1, p2 is a pullback in the category PTNets, where the transition component is not a pullback in Sets. In the cube, the bottom face is a pushout in PTNets along an injective morphism m ∈ M , all front and back faces are pullbacks, but the top face is no pushout. Hence, this cube violates the VK property. 4 AHL Schemas and Nets as Weak Adhesive HLR Categories In this section, we combine algebraic specifications with Petri nets leading to AHL schemas and nets (see [PER95]). Intuitively, an AHL net is a Petri net, where ordinary, uniform tokens are replaced by data elements from the given algebra. Firing a transition t means to remove some data elements from the input places and add some data elements, computed by term evaluation, to the output places of t. There could be also some firing conditions to restrict the firing behaviour of a transition. In addition, a typing of the places restricts the data elements which could be put on each place to that of a certain type. 5 / 13 Volume 2 (2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories t0 t′0 1,1′ 1,2′ 2,2′ 2,1′ t1 1 2 t2 1′ 2′ t3 p 2 (1) A B C D p1 p2 g2 g1 t0 t′0 1,1′ 1,2′ 2,2′ 2,1′ t1 1 2 t2 1′ 2′ t3 p 2 1,1′ 1,2′ 2,2′ 2,1′ 1 2 1′ 2′ 1m p1 p2 g2 g1 Figure 1: The pullback (1) in PTNets and the cube violating the VK property Definition 6 An AHL schema over an algebraic specification SP, where SP = (SIG, E, X ) has additional variables X and SIG = (S, OP), is given by AS = (P, T, pre, post, cond,type) with sets P and T of places and transitions, pre, post : T → (TSIG(X )⊗P) ⊕ as pre- and post-domain func- tions, cond : T → P f in(E qns(SIG, X )) assigning to each t ∈ T a finite set cond(t) of equations over SIG and X , and type : P → S a type function. Note that TSIG(X ) is the SIG-term algebra with variables X and (TSIG(X )⊗P) = {(term, p) | term ∈ TSIG(X )type(p), p ∈ P}. An AHL schema morphism f : AS → AS′ is given by a pair of functions f = ( fP : P → P ′, fT : T → T ′) which are compatible with pre, post, cond and type as shown below. P f in(E qns(SIG, X )) T (TSIG(X )⊗P) ⊕ T ′ (TSIG(X )⊗P ′)⊕ P P′ S pre post pre′ post′ cond cond′ fT (id⊗ fP) ⊕ ty pe ty pe′ fP== = Given an algebraic specification SP, AHL schemas over SP and AHL schema morphisms form the category AHLSchemas(SP). As shown in [EEPT06], AHL schemas over a fixed algebraic specification SP are a weak adhesive HLR category. Corollary 3 The category (AHLSchemas(SP), M ) is a weak adhesive HLR category. M is the class of all injective morphisms f , i.e. fP and fT are injective. Proof Idea. Since SP is fixed, the construction of pushouts and pullbacks in AHLSchemas(SP) is essentially the same as in PTNets, which is already a weak adhesive HLR category. We can apply the idea of comma categories ComCat(F, G; I ), where in our case the source functor of the operations pre, post, cond,type is always the identity IDSets, and the target functors are (TSIG(X )⊗ ) ⊕ : Sets → Sets and two constant functors. In fact, (TSIG(X )⊗ ) : Sets → Sets, the constant functors and �⊕ : Sets → Sets preserve pullbacks along injective functions. Hence also (TSIG(X )⊗ ) ⊕ : Sets → Sets preserves pullbacks along injective functions. Proc. PNGT 2006 6 / 13 ECEASST To represent the actual data space, we combine AHL schemas and algebras to AHL nets. Definition 7 An AHL net AN = (S, A) is given by an AHL schema S over SP and an SP-algebra A. An AHL net morphism f : AN → AN′ is given by a pair f = ( fS : S → S ′, fA : A → A ′), where fS is an AHL schema morphism and fA an SP-homomorphism. Given an algebraic specification SP, AHL nets over SP and AHL net morphisms form the category AHLNets(SP). Corollary 4 If (Algs(SP), M ) is a weak adhesive HLR category then the category (AHLNets(SP), M ′) is a weak adhesive HLR category. M ′ is the class of all morphisms f = ( fS, fA), where fS is injective and fA ∈ M . Proof Idea. The category AHLNets(SP) is isomorphic to the product category AHLSchemas(SP) × Algs(SP). According to Theorem 1.1 this implies that (AHLNets(SP), M ′) is a weak adhesive HLR category. Up to now, it is not clear whether the category Algs(SP) of algebras over an arbitrary spec- ification SP with the class M of injective morphisms is a weak adhesive HLR category. This has been shown in [EEPT06] only for so-called graph structure algebras, where only unary op- erations are allowed. For an arbitrary specification, we can use the class M of isomorphisms to obtain a weak adhesive HLR category. 5 Generalized AHL Schemas and Nets as Weak Adhesive HLR Categories We get a more powerful variant of AHL schemas, called generalized AHL schemas, if we do not fix the specification. This is especially useful for net transformations, where we can define rules based on a (small) specification SP, which represents the necessary data, that can be applied to nets over a (larger) specification SP′. In this section, we define generalized AHL schemas and nets, and show that they form weak adhesive HLR categories under certain conditions on the data part. Definition 8 A generalized AHL schema GS = (SP, AS) is given by an algebraic specification SP and an AHL schema AS over SP. A generalized AHL schema morphism f : GS → GS′ is a tuple f = ( fSP : SP → SP ′, fP : P → P′, fT : T → T ′), where fSP is a specification morphism and fP, fT are compatible with pre, post, cond and type. f #SP is the extension of fSP to terms and equations. P f in(E qns(SIG, X )) P f in(E qns(SIG ′, X )) T (TSIG(X )⊗P) ⊕ T ′ (TSIG′(X )⊗P ′)⊕ P P′ S S′ P f in ( f # SP) fSP,S pre post pre′ post′ cond cond′ fT ( f #SP⊗ fP) ⊕ ty pe ty pe′ fP== = Generalized AHL schemas and generalized AHL schema morphisms form the category AHLSchemas. 7 / 13 Volume 2 (2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories To show that generalized AHL schemas form a weak adhesive HLR category, we need an extension of comma categories, where we loosen the restrictions on the domain of the functors. Definition 9 Given index sets I and J , categories C j for j ∈ J and Xi for i ∈ I , and for each i ∈ I two functors Fi : Cki → Xi, Gi : C`i → Xi with ki, `i ∈ J , then the general comma category GComCat((C j) j∈J , (Fi, Gi)i∈I ; I , J ) is defined by • objects ((A j ∈ C j) j∈J , (opi)i∈I ), where opi : Fi(Aki ) → Gi(A`i ) is a morphism in Xi, • morphisms h : ((A j), (opi)) → ((A ′ j), (op ′ i)) as tuples h = ((h j : A j → A ′ j) j∈J ) such that for all i ∈ I op′i ◦Fi(hki ) = Gi(h`i )◦opi. We can extend the result from Theorem 1.4 to general comma categories, such that the general comma category is a weak adhesive HLR category under certain conditions. Theorem 2 A general comma category GC = (GComCat((C j) j∈J , (Fi, Gi)i∈I ; I , J ), M ) with M = (× j∈J M j)∩MorGC is a weak adhesive HLR category, if (C j, M j) are weak adhe- sive HLR categories for j ∈ J , and for all i ∈ I Fi preserves pushouts along Mki -morphisms and Gi preserves pullbacks along M`i -morphisms. Proof Idea. It is easy to show that M is a class of monomorphisms closed under isomorphisms, composition and decomposition since this holds for all components M j. As in normal comma categories, pushouts along M -morphisms are constructed component- wise in the underlying categories. The pushout object is the componentwise pushout object, where the operations are uniquely defined using the property that Fi preserves pushouts along Mki -morphisms. Analogously, pullbacks along M -morphisms are constructed componentwise, where the oper- ations of the pullback object are uniquely defined using the property that Gi preserves pullbacks along M`i -morphisms. The weak VK square property follows, since in a proper cube, all pushouts and pullbacks can be decomposed leading to proper cubes in the underlying categories, where the weak VK property holds. The subsequent recomposition yields the weak VK property for the general comma category. Also the restriction of a weak adhesive HLR category to a full subcategory yields a weak adhesive HLR category, if the pushouts and pullbacks over M -morphisms are preserved. Corollary 5 Given a weak adhesive HLR category (C, M ), a full subcategory (C′, M ′) of C with M ′ = M |C′ is a weak adhesive HLR category, if C ′ has pushouts and pullbacks along M ′-morphisms which are preserved by the inclusion functor. Proof Idea. By precondition, pushouts and pullbacks along M ′-morphisms in C′ exist. Obvi- ously, M ′ is a class of monomorphisms with the required properties. Since we only restrict the objects and morphisms, the weak VK square property is inherited from C. With these results, we are now able to show that the category of generalized AHL schemas is a weak adhesive HLR category. Proc. PNGT 2006 8 / 13 ECEASST Theorem 3 The category (AHLSchemas, M ) is a weak adhesive HLR category. M is the class of all morphisms f = ( fSP, fP, fT ), where fSP is a strict injective specification morphism and fP, fT are injective. Proof. The category AHLSchemas is isomorphic to a suitable full subcategory of the general comma category GC = GComCat(C1, C2, (Fi, Gi)i∈I ; I , J ) with • I = {pre, post, cond,type}, J = {1, 2}, • C1 = Specs×Sets, C2 = Sets, Xi = Sets for all i ∈ I , • Fi : C2 → Xi for i ∈{pre, post, cond}, Ftype : C1 → Xtype, Gi : C1 → Xi for all i ∈ I , where the functors are defined by • Fi = IdSets, Gi(SP, P) = (TSIG(X )×P) ⊕, Gi( fSP, fP) = ( f # SP × fP) ⊕ for i ∈{pre, post}, • Fcond = IdSets, Gcond (SP, P) = P f in(E qns(SIG, X )), Gcond ( fSP, fP) = P f in( f # SP), • Ftype(SP, P) = P, Ftype( fSP, fP) = fP, Gtype(SP, P) = S, Gtype( fSP, fP) = fSP,S. Since (Specs, M1) with the class M1 of strict injective morphisms and (Sets, M2) with the class M2 of injective morphisms are weak adhesive HLR categories, Theorem 1.1 implies that also (Specs×Sets, M1 ×M2) is a weak adhesive HLR category. The functors Fi preserve pushouts along Mki -morphisms, which is obvious for Fpre, Fpost , Fcond and shown in Corollary 6 for Ftype, and the functors Gi preserve pullbacks along M`i -morphisms as shown in Corollary 7, Corollary 8 and Corollary 9, therefore we can apply Theorem 2 such that GC is a weak adhesive HLR category. Now we restrict the objects ((SP, P), T, pre, post, cond,type) in GC to those, where (1) pre(t), post(t) ∈ (TSIG(X )⊗P) ⊕ for all t ∈ T. The full subcategory induced by these objects is isomorphic to AHLSchemas. Since the condi- tion (1) is preserved by pushout and pullback constructions in GC, it follows that for morphisms f , g ∈ AHLSchemas with the same (co)domain, the pushout (pullback) over f , g in GC is also the pushout (pullback) in AHLSchemas. With Corollary 5 we conclude that (AHLSchemas, M ) is a weak adhesive HLR category. Corollary 6 The functor H : Specs×Sets → Sets : (SP, M) 7→ M, ( fSP, fM ) 7→ fM preserves pushouts (along M1 ×M2-morphisms). Proof. In a product category, a square is a pushout if and only if the componentwise squares are pushouts in the underlying categories. Thus, if (1) is a pushout in Specs×Sets also (2) is a pushout in Sets, which means that H preserves pushouts. (SP0, M0) (SP1, M1) (SP2, M2) (SP3, M3) (1) ( fSP, fM ) (gSP,gM ) (g ′ SP,g ′ M ) ( f ′SP, f ′ M ) M0 M1 M2 M3 (2) fM gM g′M f ′M 9 / 13 Volume 2 (2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories Corollary 7 The functor H : Specs×Sets → Sets : (SP, M) 7→ S, ( fSP, fM ) 7→ fSP,S preserves pullbacks (along M1 ×M2-morphisms). Proof. In a product category, a square is a pullback if and only if the componentwise squares are pullbacks in the underlying categories. Thus, if (3) is a pullback in Specs×Sets also (4) is a pullback in Specs. In Specs, pullbacks are constructed componentwise on the signature part (with some special treatment of the equations). Thus, also (5) is a pullback in Sets, which means that H preserves pullbacks. (SP0, M0) (SP1, M1) (SP2, M2) (SP3, M3) (3) ( fSP, fM ) (gSP,gM ) (g ′ SP,g ′ M ) ( f ′SP, f ′ M ) SP0 SP1 SP2 SP3 (4) fSP gSP g′SP f ′SP S0 S1 S2 S3 (5) fSP,S gSP,S g′SP,S f ′SP,S TSIG0 (X0) TSIG1 (X1) TSIG2 (X2) TSIG3 (X3) (6) f #SP g#SP g ′# SP f ′#SP Corollary 8 The functor H : Specs×Sets → Sets : (SP, M) 7→ (TSIG(X )×M)⊕, ( fSP, fM ) 7→ ( f #SP × fM) ⊕ preserves pullbacks along M1 ×M2-morphisms. Proof. The product functor × preserves general pullbacks and, as shown in [EEPT06], the func- tor �⊕ preserves pullbacks along injective morphisms. Thus, it lasts to show that T : Specs → Sets : SP 7→ TSIG(X ), where we forget the type information of the terms, preserves pullbacks. In Specs, the pullback (4) is constructed componentwise on the sorts, operations and variables, which means that S0 = {(s1, s2) | g ′ SP,S(s1) = f ′ SP,S(s2)}, OP0 = {(op1, op2) : (s 1 1, s 1 2)...(s n 1, s n 2) → (s1, s2) | g ′ SP,OP(op1 : s 1 1...s n 1 → s1) = f ′ SP,OP(op2 : s 1 2...s n 2 → s2)} and X0 = {(x1, x2) | g ′ SP,X (x1) = f ′SP,X (x2)}. Therefore, the terms in TSIG0 (X0) are defined by TSIG0,s(X0) = X0,s ∪{(c1, c2) | (c1, c2) :→ s ∈ OP0}∪{(op1, op2)(t1, ..,tn) | (op1, op2) : s1...sn → s ∈ OP0,ti ∈ TSIG0,si (X0)}. We have to show that TSIG0 (X0) is isomorphic to the pullback object P over f ′# SP and g ′# SP with P = {(t1,t2) | g ′# SP(t1) = f ′# SP(t2)}. Since P is a pullback, with f ′# SP ◦ g # SP = g ′# SP ◦ f # SP we get an induced morphism i : TSIG0 (X0) → P with i(t) = ( f # SP(t), g # SP(t)), which means that i is inductively defined by i(c1, c2) = (c1, c2) for constants, i(x1, x2) = (x1, x2) for variables and i((op1, op2)(t1, ...,tn)) = (op1(i(t1)1, ..., i(tn)1), op2(i(t1)2, ..., i(tn)2)) for complex terms. f ′SP, g ′ SP are specification morphisms and f ′# SP, g ′# SP are inductively defined on terms. This means, for a pair (t1,t2) ∈ P, the terms t1 and t2 have to have the same structure. Define j : P → TSIG0 (X0) inductively by j(c1, c2) = (c1, c2) for constants, j(x1, x2) = (x1, x2) for variables and j(op1(t 1 1 , ...,t n 1 ), op2(t 1 2 , ...,t n 2 )) = (op1, op2)( j(t 1 1 ,t 1 2 ), ..., j(t n 1 ,t n 2 )) for complex terms. By induction, it can be shown that i◦ j = idP and j◦i = idTSIG0 (X0) . This means that i and j are isomorphisms and (6) is a pullback in Sets. Corollary 9 The functor H : Specs×Sets→Sets : (SP, M) 7→P f in(E qns(SIG, X )), ( fSP, fM) 7→ P f in( f # SP) preserves pullbacks along M1 ×M2-morphisms. Proof. In [EEPT06], it is shown that P preserves pullbacks along injective morphisms. Analo- gously, this can be shown for P f in, since if we start the construction for finite sets, this property is preserved. Thus, it lasts to show that E qns preserves pullbacks, which can be proven similar to the proof for sets of terms in Corollary 8 above. Proc. PNGT 2006 10 / 13 ECEASST x l(x)⊕r(x) xx x l(x)⊕r(x) think:phil eat:phil table: f orkput take sorts : phil, f ork opns : p1, ..., pn :→ phil f1, ..., fn :→ f ork l, r : phil → f ork eqns : l(pi) = fi ∀i = 1, ..., n r(pi) = fi+1 ∀i = 1, ..., n−1 r(pn) = f1 Figure 2: The AHL net for n dining philosophers As previously, we combine generalized AHL schemas and algebras to generalized AHL nets. Definition 10 A generalized AHL net GN = (GS, A) is given by a generalized AHL schema GN over the algebraic specification SP and an SP-algebra A. A generalized AHL net morphism f : GN → GN′ is a tuple f = ( fGS : GS → GS ′, fA : A → VfSP (A ′)), where fGS is a generalized AHL schema morphism and fA an algebra homomorphism. VfSP : Algs(SP ′) → Algs(SP) is the forgetful functor induced by fSP. Generalized AHL nets and generalized AHL net morphisms form the category AHLNets. Corollary 10 If the category (Algs, M1) of all algebras and generalized homomorphisms is a weak adhesive HLR category, then also the category (AHLNets, M ) is a weak adhesive HLR category. M is the class of all injective AHL net morphisms f with fA ∈ M1. Proof Idea. The category AHLNets is isomorphic to the full subcategory (AHLSchemas×Algs)|Ob′, where Ob ′ = {((SP, P, T, pre, post, cond,type), A) | A ∈ Algs(SP)}. In this subcategory, the pushout and pullback objects over M -morphisms are the same as in AHLSchemas×Algs. According to Theorem 1.1 and Corollary 5 this implies that (AHLNets, M ) is a weak adhesive HLR category. Up to now we do not know whether the category (Algs, M1) with the class M1 of injective morphisms is a weak adhesive HLR category. But if we restrict M1 to isomorphisms, (Algs, M1) is a weak adhesive HLR category and M1 is already a useful class for rules in net transformation systems. In many cases, one does not want to change the specification and algebra within the rule (where M1-morphisms are necessary). But for the match, general morphisms are allowed, thus we can apply such a rule to nets over different specifications and with different algebras. Another possibility is to restrict the algebra part to quotient term algebras leading to the category Algs|QTA with objects (SP, TSP) and morphisms f = ( fSP, fT ) : (SP, TSP) → (SP ′, TSP′) with fSP : SP → SP′ and fT : TSP → VfSP (TSP′) uniquely determined. Algs|QTA is isomorphic to the category of specifications and thus, together with strict injective morphisms, a weak adhesive HLR category. In the following, we present an example based on the well-known Dining Philosophers Prob- lem (see [BEE01]), where the behaviour of the philosophers is modeled by a net, while the philosophers themselves are modeled within the data structure. Example 2 For n philosophers, the AHL net with its specification is given in Figure 2. For the 11 / 13 Volume 2 (2006) Algebraic High-Level Nets as Weak Adhesive HLR Categories x xf av(x) f av(x)x xthink:phil think:phil think:phil read:phil lib:book get returnsorts: phil sorts: phil sorts: phil,book opns: f av:phil→book L K R l r x x f av(x)f av(x) x x x l(x)⊕r(x) xx x l(x)⊕r(x) read:phil lib:book think:phil eat:phil table: f orkput take return get sorts : phil, f ork, book opns : p1, ..., pn :→ phil f1, ..., fn :→ f ork l, r : phil → f ork f av : phil → book eqns : l(pi) = fi ∀i = 1, ..., n r(pi) = fi+1 ∀i = 1, ..., n−1 r(pn) = f1 Figure 3: The production and the result of the direct transformation data part, we use the quotient term algebra. Each philosopher pi has a left fork fi and a right fork fi+1, except pn with the right fork f1, and needs these two forks to eat. In the AHL net, this condition is assured by the pre- and post-domain functions. In the top of Figure 3 an examplary production is shown, where we extend the possible behav- iour of the philosophers. We introduce a library, where a philosopher pi may go to and get his favourite book f av(pi) to read. Due to our developed theory, this very simple rule can be applied to all kinds of nets, independent from the number of philosophers. In the bottom, the application of this rule to the AHL net in Figure 2 is shown, where the library has been introduced. Note that also the specification has changed, since the new sort book and the operation f av have been added. Now a thinking philosophers may go to the library by firing the new transition get. 6 Conclusion and Future Work In this paper we have shown that all kinds of algebraic high-level schemas and nets are weak adhesive HLR categories. This means, that we can apply the theory for graph transformations developed in [EEPT06] also to different kinds of net transformations based on AHL schemas and nets. At the moment, the available data structure underlying the AHL nets is restricted to a few, but still interesting cases. More work is needed in the area of algebras, where the categories Algs(SP) of algebras over a certain specification SP and Algs of generalized algebras and homo- morphisms should be verified to be weak adhesive HLR categories, likely under some restrictions on the specification or M -morphisms. The category Algs is equivalent to a Grothendieck cat- egory (see [TBG91]) indexed over the category Specs. Grothendieck categories have general pushouts and pullbacks, if so have the underlying categories, but they have not been shown to be Proc. PNGT 2006 12 / 13 ECEASST weak adhesive HLR categories. A step towards this has been made in [EOP06], where also some restrictions to the morphism class M are discussed which could lead to a suitable weak adhesive HLR category. Bibliography [BEE01] R. Bardohl, C. Ermel, H. Ehrig. Generic Description of Syntax, Behavior and Ani- mation of Visual Models. Technical report 19, TU Berlin, 2001. [EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Trans- formation. EATCS Monographs. Springer, 2006. [EHKP91] H. Ehrig, A. Habel, H. Kreowski, F. Parisi-Presicce. Parallelism and Concurrency in High-Level Replacement Systems. Mathematical Structures in Computer Science 1(3):361–404, 1991. [EHPP06] H. Ehrig, A. Habel, J. Padberg, U. Prange. Adhesive High-Level Replacement Sys- tems: A New Categorical Framework for Graph Transformation. Fundamenta Infor- maticae 74(1):1–29, 2006. [Ehr79] H. Ehrig. Introduction to the Algebraic Theory of Graph Grammars (A Survey). In Claus et al. (eds.), Graph Grammars and their Application to Computer Science and Biology. LNCS 73, pp. 1–69. Springer, 1979. [EOP06] H. Ehrig, F. Orejas, U. Prange. Categorical Foundations of Distributed Graph Trans- formation. In Corradini et al. (eds.), Graph Transformations. Proceedings of ICGT 2006. LNCS 4178, pp. 215–229. Springer, 2006. [EP06] H. Ehrig, U. Prange. Weak Adhesive High-Level Replacement Categories and Sys- tems: A Unifying Framework for Graph and Petri Net Transformations. In Futatsugi et al. (eds.), Algebra, Meaning and Computation. Essays Dedicated to J.A. Goguen. LNCS 4060, pp. 235–251. Springer, 2006. [LS05] S. Lack, P. Sobociński. Adhesive and Quasiadhesive Categories. Theoretical Infor- matics and Applications 39(3):511–546, 2005. [MM90] J. Meseguer, U. Montanari. Petri Nets are Monoids. Information and Computation 88(2):105–155, 1990. [Pad96] J. Padberg. Abstract Petri Nets: A Uniform Approach and Rule-Based Refinement. PhD thesis, TU Berlin, 1996. [PER95] J. Padberg, H. Ehrig, L. Ribeiro. Algebraic High-Level Net Transformation Systems. Mathematical Structures in Computer Science 5(2):217–256, 1995. [TBG91] A. Tarlecki, R. Burstall, J. Goguen. Some Fundamental Algebraic Tools for the Se- mantics of Computation: Part 3: Indexed Categories. Theoretical Computer Science 91(2):239–264, 1991. 13 / 13 Volume 2 (2006)