Simulating Multigraph Transformations Using Simple Graphs Electronic Communications of the EASST Volume 6 (2007) Proceedings of the Sixth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2007) Simulating Multigraph Transformations Using Simple Graphs Iovka Boneva, Frank Hermann, Harmen Kastenberg, and Arend Rensink 14 pages Guest Editors: Karsten Ehrig, Holger Giese 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 Simulating Multigraph Transformations Using Simple Graphs Iovka Boneva1, Frank Hermann2, Harmen Kastenberg1, and Arend Rensink1 1 bonevai, h.kastenberg, rensink [at] cs.utwente.nl Department of Computer Science, University of Twente P.O. Box 217, NL-7500 AE Enschede, The Netherlands 2frank [at] cs.tu-berlin.de Department of Electrical Engineering and Computer Science Technical University of Berlin, D-10587 Berlin, Germany Abstract: Application of graph transformations for software verification and model transformation is an emergent field of research. In particular, graph transformation approaches provide a natural way of modelling object oriented systems and seman- tics of object-oriented languages. There exist a number of tools for graph transformations that are often specialised in a particular kind of graphs and/or graph transformation approaches, depending on the desired application domain. The main drawback of this diversity is the lack of interoperability. In this paper we show how (typed) multigraph production systems can be translated into (typed) simple-graph production systems. The presented construction enables the use of multigraphs with DPO transformation approach in tools that only support simple graphs with SPO transformation approach, e.g. the GROOVE tool. Keywords: graph transformations, graph transformation tools, tool interoperability, multigraphs, simple graphs 1 Introduction Application of graph transformations for software verification and model transformation is an emergent field of research. In particular, graph transformation approaches provide a natural way of modelling object oriented systems and semantics of object-oriented languages [KKR06] or graphical modelling languages such as the UML [OMG05], see for instance [Hau06]. For performing the actual graph transformations, different approaches are around ranging from hyperedge replacement approach (see e.g. [DKH97]), logic based approach (see e.g. [Cou97]) to different algebraic approaches such as Single Pushout (SPO) [EHK+97] and Double Pushout (DPO) [CMR+97] approach. These different approaches all have specific application areas in which their features are used in an optimal fashion. Another difference is the use of either multigraphs or simple graphs for modelling the applica- tion domain. Whereas the former is more general, the latter suites better when using graphs for representing relations between objects in order to reason about these objects using (first-order) logical formulae [Ren04b]. While SPO can be applied for both multigraphs and simple graphs, DPO is not defined for simple graphs in general. 1 / 14 Volume 6 (2007) mailto:bonevai, h.kastenberg, rensink [at] cs.utwente.nl mailto:frank [at] cs.tu-berlin.de Simulating Multigraph Transformations For most tools performing graph transformations, the graph representation formalism and the transformation approach are determined by the targeted application domain. For instance, the GROOVE tool [Ren04a] is designed for modelling dynamic systems and verifying properties about their behaviour by generating all possible system configurations. GROOVE uses sim- ple graphs and performs SPO based graph transformations. Another example is the AGG tool [TER99] which handles multigraphs with SPO and is used e.g. for independence and termination analysis on graph grammars. The main drawback of this diversity in tools is their poor interoperability. One attempt to bridge this gap is the introduction of a common language used for exchanging models among tools, called the Graph eXchange Language (or GXL for short) [SSHW]. In order to extend this work for also exchanging the transformation specifications, GTXL [Tae01] has been proposed. However, since every implementation of a specific approach is not aware of details of other approaches, it is very difficult to include all the features in one common standard and thereby enable tools to perform semantically equivalent transformations. In a previous work [HKM06] we have proposed translations of graph production systems between GROOVE and AGG, but these translations were too specific and are not applicable in a more general context. Moreover, these translations were not invertible. In the current paper, we generalise these translations to a context that is tool independent. We show how one can encode typed multigraph production systems into simple-graph production systems, and simulate DPO transformations of multigraphs with SPO transformations on simple graphs. Then we shortly discuss how DPO transformations for multigraphs can be handled by a tool supporting only SPO on simple graphs. These results should allow, for instance, to use the GROOVE tool (or any other tool using simple graphs) with multigraphs. As a further extension, we believe that it would be possible to apply the theory of Subobject Transformation Systems [CHS06] in GROOVE. Running Example. Throughout this paper we will clarify our ideas and results using a simple example. In the example we model the dynamic behaviour of Lists and Objects that can be elements of some specific Lists. One Object may occur in a List several times. We assume that Objects can be created instantly by the environment (which we do not model in this example). Once Objects are around, different actions can be performed on Lists and Objects, like adding Objects to Lists and moving, removing or copying Objects. Fig. 1 depicts a possible configuration with two Lists: one containing a single Object and another having two entries referring to the same Object. In each configuration we assume that all List- and Object-instances have their own identity, although we do not show these identities. entryentry Object Object entry List List Figure 1: Example configuration of Lists and Objects. Proc. GT-VMT 2007 2 / 14 ECEASST Organisation of the Paper. The remaining of the paper is structured as follows. In Section 2 we provide a formal basis for the rest of the paper. In Section 3 we define our translation of multi- graphs to simple graphs and prove the equivalence of DPO transformations on multigraphs on the one hand, and SPO transformations on (special) simple graphs on the other hand. In Section 4 we describe how this equivalence can be extended to typed/labelled graphs. Then, in Section 5 we describe how DPO transformations on multigraphs can be handled by tools implementing the SPO transformation approach, such as the GROOVE tool. Finally, in Section 6 concludes and gives some hints on the way we would like to use the results of this work for improving state space exploration in GROOVE. 2 Background 2.1 Graphs and Graph Morphisms Graphs are a very powerful means of modelling systems and their behaviour. As will become clear in this paper, in some cases it is very important which notion of graphs is used, since the theory applied may depend on this choice quite heavily. The graph concept is differently interpreted by people working in different domains or even in the same domain. Graphs can e.g. be deterministic, directed or labelled. In this paper we will explicitly distinguish between what we call multigraphs and simple graphs. Definition 1 (multigraph, multigraph morphism) A multigraph is a tuple G =〈VG, EG, srcG, tgtG〉 where: • VG is a set of nodes (or vertexes); • EG is a set of edges; • srcG, tgtG : EG→VG are source and target functions. A multigraph morphism f : G→H is a pair 〈 fV , fE〉, where fV : VG →VH and fE : EG →EH are functions compatible with src and tgt functions, i.e. • fV ◦srcG = srcH ◦ fE ; • fV ◦tgtG = tgtH ◦ fE . � Definition 2 (simple graph, simple graph morphism) Let Lab be a finite set of labels. A simple graph labelled over Lab is a tuple G = 〈VG, EG〉 where • VG is a set of nodes (or vertexes); • EG ⊆VG ×Lab×VG is a set of edges. The source and target functions srcG, tgtG : EG →VG are defined for any edge e = (v, l, v ′) ∈ EG by srcG(e) = v and tgtG(e) = v ′. A simple graph morphism f : G→H is a pair 〈 fV , fE〉, where fV : VG →VH and fE : EG→EH are functions compatible with src and tgt functions and with labelling, i.e. for any edge (v, l, v′)∈ EG, fE ((v, l, v ′)) = ( fV (v), l, fV (v ′)). � 3 / 14 Volume 6 (2007) Simulating Multigraph Transformations In the sequel we will call a graph morphism f : G→ H total if its components fV and fE are total functions, and partial if its components are total functions from G′ to H , where G′ is some subgraph of G. An injective morphism is a morphism induced by injective functions. We will denote the set of multigraphs as M G and the set of simple graphs over Lab as S G (Lab). Hereafter, we will use the term graph to designate either a multigraph or a simple graph. In our formal definitions we use unlabelled multigraphs and labelled simple graphs. We start with unlabelled multigraphs in order to keep proofs simple. However, all results of the paper can be extended to labelled graphs, as it will be discussed in Section 4. Therefore, our examples will already freely use labels on both nodes and edges. 2.2 Graph Transformations When modelling system states as graphs, the dynamics of the system can be specified by graph transformations. The changes of states are then described by graph productions, also called graph transformation rules. Definition 3 (graph production) A graph production p consists of two graphs L and R, being its left-hand-side and right-hand-side, respectively, together with a partial graph morphism from L to R, called the rule morphism. We often denote a graph production p as p : L→R, also using p when referring to the rule morphism. When combining a graph G with a set P of graph productions, we get a graph pro- duction system GPS = 〈G, P〉. In a graph production system, G is called the start graph. By applying graph productions to G we can derive other graphs. The applications of graph produc- tions are defined on categories in which the objects are multigraphs or simple graphs and the arrows are the corresponding graph morphisms. For an introduction to category theory, see e.g. [BW95]. Whether a rule is applicable and to what resulting graph a derivation leads depends on the particular graph transformation approach being applied. In this paper we distinguish between the Single Pushout (SPO) [EHK+97] and the Double Pushout (DPO) [CMR+97] approach. For applying a production in the SPO approach, we only need an occurrence of the left-hand-side of the graph production. When the application of a graph production would delete a node but not all of its adjacent edges, those dangling edges will also be removed. Furthermore, if the application prescribes one node (or edge) to be both deleted and preserved, this conflict is solved in favour of deletion. These conflicts are resolved in the DPO approach by forbidding such applications of productions, i.e. the DPO approach requires additional conditions on the applications which are called the dangling edge condition and the identification condition (together referred to as the gluing condition). In the DPO approach, a graph production p : L→R is depicted as a span L l ← K r → R of total graph morphisms, such that K = L∩R, l : dom(p)→L, and r : dom(p)→R. To be determin- istic, it is necessary that either rule morphisms or matchings are injective. We will now define applications of graph productions and the corresponding derivations for both SPO and DPO. Definition 4 (derivation) Given a graph production p : L→R and a graph G, a total graph mor- phism m : L→G is called matching. The direct derivation from a graph G to a graph H through Proc. GT-VMT 2007 4 / 14 ECEASST the production p via matching m, denoted G = p,m =⇒ H , is constructed: (SPO) as the pushout of p and m in the category of graphs and partial graph morphisms (see Fig. 2(a)); (DPO) by taking, in the category of graphs and total graph morphisms, first the pushout comple- ment D (with k : K→D and l∗: D→G) of l and m, if it exists (ensured by the gluing condition), and then the pushout of r and k (see Fig. 2(b)). � L p / m �� (PO) R m∗ �� G p∗ / H (a) SPO L m �� (PO) K l oo r // k �� (PO) R m∗ �� G D l∗ oo r∗ // H (b) DPO Figure 2: Graph H as the result of an SPO and a DPO derivation. Intuitively, applying a graph production p to a graph G can be seen as a sequence of two actions: find an occurrence (matching) of L in G and then replace that occurrence by R. This then results in the graph H . An example direct derivation is shown in Fig. 4. An important difference between SPO and DPO is the fact that DPO does not work on simple graphs with arbitrary matchings, because in some cases the required pushout construction is not unique or does not exist. In this paper we do apply DPO on simple graphs, but then ensure that we restrict to a special class of matchings and/or morphisms. This issue will be discussed in Section 3. 2.3 Back to the Example Now that we have introduced the notion of graphs and the graph transformation technique, we can recall the example and give a formal description of the actions. In Fig. 3 we specify some of the actions from the example as graph transformation rules by showing their left-hand-side and right-hand-side graph. The rule morphisms in Fig. 3 are defined by the placing of the elements. entry ListList R Object p L Object (a) add p L Object List entry List R Object entry List entry List (b) copy Figure 3: Graph transformation rules for some of the actions in the example. In Fig. 4 we show a single (SPO) rule application in which we apply the copy-rule (Fig. 3(b)) on a graph G consisting of two Lists each containing one Object, also showing the resulting graph H . 5 / 14 Volume 6 (2007) Simulating Multigraph Transformations List entry List entry List entry List entry List entry List Object List entry entry m p* m* p G H RL entry Object Object ObjectObject Object List Figure 4: An example direct derivation. 3 From Multigraphs to Simple Graphs and back again In this section we describe our translation between multigraphs and simple graphs. At a categor- ical level we will show that these translations are functors which are isomorphisms, moreover being each others inverse. 3.1 From Multigraphs to Simple Graphs Consider the set of labels LMG = {s, t}. The function Sim maps multigraphs from M G into simple graphs in S G (LMG) as follows: every edge e in the multigraph with source node vs and target node vt becomes a special node (this we call a proxy node) with two outgoing edges (e, s, vs) and (e, t, vt). Thus, we will use e as a variable ranging over edges of multigraphs and proxy nodes in simple graphs. Fig. 5 shows an example applying the Sim function. Formally, let G = 〈VG, EG, srcG, tgtG〉 be a multigraph. Then Sim(G) is the graph H = 〈VH , EH〉 with • VH = VG ∪EG, that is, edges of G are nodes in H ; • EH = ⋃ e∈EG {(e, s, srcG(e)), (e, t, tgtG(e))}. The Sim function can be extended on graph morphisms. That is, if G and H are multigraphs and m : G→H is a morphism, then Sim(m) : Sim(G)→Sim(H) is the morphism defined by 1: • for all v in VSim(G) (i.e. v ∈VG ∪EG), (Sim(m))(v) = m(v); • for all (e, l, v) in ESim(G), (Sim(m))((e, l, v)) = (m(e), l, m(v)). Note that the definition of Sim(m) on edges of Sim(G) ensures that Sim(m) is indeed a simple graph morphism. 1 In this definition m is supposed to be a total morphism. This is not a restriction as a partial morphism is a total morphism on a subgraph. Proc. GT-VMT 2007 6 / 14 ECEASST t s s t Figure 5: Encoding of a multigraph (on the left) into simple graphs with proxy nodes (on the right) by the Sim function. 3.2 From Simple Graphs to Multigraphs Let S G M G be the set of bipartite simple graphs over LMG satisfying the following conditions: G = (V, E) ∈ S G M G if 1. V = Vn ∪Ve where Vn and Ve are two disjoint sets; 2. E = Es∪Et where Es and Et are disjoint sets and Es ⊆Ve×{s}×Vn, and Et ⊆Ve×{t}×Vn; 3. any node e in Ve has exactly two adjacent edges (e, s, v ′ n)∈Es and (e, t, v ′′ n ) for some v ′ n, v ′′ n ∈ Vn. We now define the function Sim−1 : S G M G →M G as follows: if G = 〈Vn ∪Ve, EG〉 where Vn and Ve are as in the description of S G M G stated above, then H = Sim −1(G) is the graph 〈V, E, src, tgt〉 such that V = Vn, E = Ve, and for any e ∈ E , src(e) = vs and tgt(e) = vt, where vs, vt ∈Vn are the nodes such that (e, s, vs), (e, t, vt)∈EG. We know by condition 3 of the definition of the set of graphs S G M G that the nodes vs and vt exist and are unique. The Sim−1 function can also be extended on graph morphisms. If m : G→H is a simple graph morphism, then Sim−1(m) : Sim−1(G)→Sim−1(H) is the multigraph morphism such that for any x in VG, (Sim −1(m))(x) = m(x). We now show that Sim−1(m) defined this way is indeed a multigraph morphism. Let G′ = Sim−1(G), H′ = Sim−1(H) and m′ = Sim−1(m). Then for any edge e ∈ EG′, (m ′◦ srcG′)(e) = m(vs) where vs is the unique node in G such that (e, s, vs) is an edge of G. As m is a simple graph morphism, (m(e), s, m(vs)) is an edge in H . On the other hand, (srcH′ ◦m ′)(e) = srcH′(m(e)) is the unique node v ′ s in H such that (m(e), s, v ′ s) is a edge in H . We deduce then that both (m(e), s, v′s) and (m(e), s, m(vs)) are edges in H . By uniqueness of v ′ s, necessarily v ′ s = m(vs), so m′◦srcG′ = srcH′ ◦m ′. We can see in a similar way that m′◦tgtG′ = tgtH′ ◦m ′. It is not very hard to see that S G M G is exactly the set of simple graphs that are images of multigraphs by the Sim function, and that the function Sim−1 is the inverse of the function Sim. This will be formally stated in the following section. 3.3 Categories for Multigraphs and Simple Graphs In this section we define the categories MG and SGMG(LMG) on which DPO transformation is defined for multigraphs and for simple graphs that are encodings of multigraphs. We show also that the functions Sim and Sim−1 define free functors from MG to SGMG(LMG) and from 7 / 14 Volume 6 (2007) Simulating Multigraph Transformations SGMG(LMG) to MG respectively. This will guarantee that performing DPO transformations on multigraphs can be simulated by DPO transformations on simple graphs that belong to S G M G , as stated in Theorem 1. The reader who is not familiar with category theory will probably only be interested in the result of this theorem. Definition 5 (categories MG, SG(L), and SGMG(LMG)) MG is the category whose objects are elements of M G and whose arrows are multigraph morphisms. SG(L) is the category whose objects are simple graphs over the set of labels L and whose arrows are simple graph morphisms. Finally, SGMG(LMG) is the category whose objects are elements of S G M G and whose arrows are simple graph morphisms. Note that SGMG(LMG) can be equivalently defined as the full subcategory of SG(LMG) in- duced by S G M G . Recall that a functor f =〈 fo, fm〉 from a category C to a category D is a function with fo (resp. fm) associating objects (resp. morphisms) of D with objects (resp. morphisms) of C and such that f preserves morphisms, identities and composition. The following lemma easily follows from the definitions. Lemma 1 It holds that 1. Sim is a functor from MG to SGMG(LMG) and 2. Sim−1 is a functor from SGMG(LMG) to MG; 3. the functors Sim and Sim−1 are isomorphisms: Sim◦Sim−1 = IDSGMG(LMG) and Sim −1 ◦Sim = IDMG. Graph morphisms are called edge reflecting if edges are reflected along their boundary, i.e. whenever there is an edge between two nodes in the image of the morphism, there should be an edge between the pre-images of these nodes in the domain of the morphism (see next lemma). Lemma 2 All morphisms f : G → H in SGMG(LMG) are edge reflecting, i.e. if ( f (x), l, f (y)) ∈ EH then (x, l, y) ∈ EG. Proof. It is enough to show that Sim translates to edge reflecting morphisms, because the cat- egories are isomorphic. By definition, Sim translates edges to special nodes with two outgoing edges to other nodes. Nodes in MG are connected via structured edges in SGMG(LMG), thus edges connect an original node with a proxy node. Let f be a graph morphism in MG. If Sim( f ) reaches a proxy node, f has to map to the original edge. Therefore, also the adjacent edges are reached by Sim( f ) and thus, Sim( f ) is edge reflecting. 3.4 Multigraph versus Simple Graph transformations In the sequel we combine the graph categories MG, SGMG(LMG) and SG(LMG) with the trans- formation approaches SPO and DPO. We will denote such combinations with MG+DPO etc. The Proc. GT-VMT 2007 8 / 14 ECEASST aim of this paper is to translate MG+DPO into SG(LMG)+SPO. This is achieved in two steps: MG+DPO → SGMG(LMG)+DPO → SG(LMG)+SPO The first step consists in encoding multigraphs and production rules using the Sim function, thus obtaining simple graphs in S G M G and simple graph morphisms. The second step consists in encoding the DPO rules into SPO rules. In [HHT96] (Proposition 3.5) it has been shown that it is possible to translate the application conditions of a DPO derivation (i.e. dangling edge and identification condition) in MG to equivalent negative application conditions (NACs) for performing SPO derivations in MG. In Theorem 1 we show that the initial DPO transformations in MG can be simulated by the translated SPO transformation in SG(LMG). Remark 1 (Uniqueness of derivations) To be deterministic for given graph production and matching, DPO derivations need the uniqueness of pushout complements. In adhesive categories this is the case if the rule morphisms are, or the match is, monomorphic (see Lemma 15 in [LS04]), meaning injective in the category Graph. In our setting, the category MG is adhesive and therefore also SGMG(LMG) is, because it is isomorphic. The monomorphisms in the lat- ter one are also equalisers by their property of being edge reflecting and thus, they are regular monomorphisms. Given a DPO rule p = L l ← K r → R, we use Sim(p) to denote Sim(L) Sim(l) ← Sim(K) Sim(r) → Sim(R), and we denote by Sim∗(p) the translated rule equipped with additional NACs, as de- scribed in [HHT96]. For the following lemma we interpret graphs of SGMG(LMG) as graphs in MG by forgetting all labels. This allows us to show that pushouts are not only translated to those in a different category, but also remain pushouts in the original category of multigraphs, after applying Sim. An extension of MG with labels is direct and only adds information, which does not interfere with the pushout construction. Lemma 3 A // �� (PO) B �� C // D in MG implies Sim(A) // �� (PO) Sim(B) �� Sim(C) // Sim(D) in MG up to label information. Proof. (sketch) Pushouts in MG are constructed component-wise for the sets of edges and nodes by building the disjoint union and factorising along the equivalence generated by the span of morphisms. The definition of Sim is compatible with the standard pushout construction, i.e. Sim(D) = Sim(B +A C) ∼= Sim(B) +Sim(A) Sim(C). Theorem 1 (simulation) Given a rule p = L l ← K r → R and a match m : L → G in MG, where l is injective, the following three are equivalent: 1. G = p,m =⇒DP O G ′ in MG; 2. Sim(G) = Sim(p),Sim(m) ========⇒DP O Sim(G ′) in SGMG(LMG); 9 / 14 Volume 6 (2007) Simulating Multigraph Transformations 3. Sim(G) = Sim∗(p),Sim(m) =========⇒S P O Sim(G ′) in SG(LMG). Furthermore, if a rule in 2 or 3 is applicable, then the result is always a graph in SG(LMG). Proof. 1 ⇔ 2 Sim and Sim−1 are isomorphisms by Lemma 1 and hence, they preserve all Limits and Colimits. Since l is injective the DPO-derivations are unique up to isomorphism. 2 ⇒ 3 The derivation in 2 can be considered as a derivation in MG up to labels, according to Lemma 3. Then using [HHT96], it is equivalent to an SPO derivation with NACs in MG with result Sim(G′), that is, Sim(G′) is the pushout of p and m in MG. But, as Sim(G′) is a simple graph, it is also the pushout of p and m in SG(LMG), up to labels. Because of the strict relation between the labels in graphs in S G M G and their structure, it is not difficult to see that Sim(G′) is also the pushout of p and m in SG(LMG) without ignoring the labels. 3 ⇒ 2 Let H′ be the result of the derivation (a) Sim(G) = Sim∗(p),Sim(m) =========⇒S P O H ′ in MG. By [HHT96] we know that then (b) Sim(G) = Sim(p),Sim(m) ========⇒DP O H ′ is a derivation in MG. Since Sim(p), Sim(m) are morphisms in SGMG(LMG), by Lemma 2 we know that they are edge reflecting, and this allows to deduce that the graph H′ is a simple graph, that is, an object of SG(LMG). Now, as SG(LMG) is a full subcategory of MG and by (a), we have that H′ is the pushout of Sim∗(p) and Sim(m) in SG(LMG). By uniqueness of this pushout and the derivation in point 3 we deduce that H′ = H , thus (b) is a derivation in SG(LMG). Finally, one can see that H′ and the context graph in (b) are also objects of SGMG(LMG) because the translated rule will only produce and delete complete structured edges by definition of Sim. Hence, no garbage (i.e. proxy nodes with either an outgoing s-edge or a t-edge, but not both) will occur. Thus, (b) is also a derivation in SGMG(LMG). Result H ∼= Sim(G′) is a direct consequence of the last part of the proof for the previous item. 4 Extensions Theorem 1 immediately extends to rules with negative application conditions, because they con- tain just additional graphs and morphisms of the same kind. Thus, we will not describe this aspect in more detail. We are also confident that the results from this paper can be extended in a straightforward manner to hypergraphs [Kön02], which differ from multigraphs in not having source and target functions, but rather a single function ends : EG →V ∗ G that associates with every edge a string of nodes. Hypergraphs can be translated to simple graphs using precisely the same technique of encoding edges as proxy nodes, with in this case as many auxiliary edges (to nodes) as there are elements in ends(e). Up to now we have only considered unlabelled and untyped multigraphs, but all the results that we have shown can be easily extended to typed multigraphs, and hence to labelled ones, since labelling can be insured by typing; see, e.g., [EEPT06]. Fig. 6 shows how one of our example labelled multigraphs would be encoded into a simple graph. Proc. GT-VMT 2007 10 / 14 ECEASST entry t s tentry s List Object entry entry List Object Figure 6: Encoding of a labelled multigraph. A typed graph 〈G, m〉 is a graph G together with a morphism m : G → TG to some graph TG called the type graph. A typed graph morphism f : 〈G, m〉→〈G′, m′〉 is a morphism for which m = m′◦ f . Transformations of typed graphs should involve only typed graph morphisms. It is equivalent to consider transformations in a slice category. That is, typed transformations in C w.r.t. the type graph TG are equivalent to transformations in the slice category C ↓ TG, where C is either MG or SGMG(LMG) and TG is a multigraph or simple graph, respectively. Now, as MG and SGMG(LMG) are isomorphic with Sim as isomorphism functor, it is trivial to see that the slice categories are also isomorphic. Thus, there is a pushout in MG ↓ TG if, and only if, there is a pushout in SGMG(LMG) ↓ Sim(TG). Then the simulation result stated in Theorem 1 also holds for a typed transformation. However, in this case, an additional translation step is still required to translate to untyped simple graphs. Then we have to extend the labels to encode the typing; hence, the translation is from [SGMG(LMG) ↓ Sim(TG)]+SPO to [SGMG(LMG ×(VT G ∪ET G))]+SPO. We are convinced that this translation is straightforward, but we have not given the proof. 5 Simulation in SPO Tools Tools performing graph transformations often implement SPO since this requires only one pushout construction whether for DPO an additional pushout complement construction is needed. Prob- lems arise when performing rule applications using SPO that do not satisfy the gluing condition. In the running example such a situation would occur when applying the delete rule on an Object that is contained in more than one List. In order still to be able to perform DPO transformation, there are basically two alternatives: 1. restrict rule applications by checking the gluing condition after searching for matchings; 2. encode the gluing condition using additional negative application conditions in the trans- formation rules. Choosing the first alternative requires that the tool performs an additional gluing check on the found matches. This gluing check means that for all identifications in the matching and for all node deletions we need to ensure that there is no preserve-delete conflict (identification condition) and that the node-deletions do not cause dangling edges (dangling condition), respec- tively. The AGG tool’s kernel implements SPO and uses a similar mechanism for handling DPO transformations. 11 / 14 Volume 6 (2007) Simulating Multigraph Transformations The second alternative is based on Theorem 1, in which we show that it is possible to sim- ulate DPO on our special simple graphs by adding additional negative application conditions as described in [HHT96]. Let us now briefly describe how one can use the GROOVE tool (or some other tool support- ing simple graph transformations with SPO) for performing DPO transformations on multigraphs. Given a (multi-) graph production system (GPS) T = 〈G, P〉, one first has to create the produc- tion system Sim(T ) by encoding the graph G and all graphs and morphisms that are parts of the productions in P in the manner described in Section 3. Note that if some productions include negative application conditions, these conditions together with the morphisms that relate them to the corresponding production are encoded just as normal graphs and morphisms. Now, if the tool offers the possibility to check for the gluing condition (choice 1 above), then the GPS Sim(T ) can be submitted to the tool, specifying that the check for the gluing condition has to be performed. Otherwise (choice 2 above), one has to construct the production system Sim∗(T ) by augmenting Sim(T ) with additional NACs for encoding the gluing condition in Sim(T ). The GPS Sim∗(T ) is then submitted to the tool as a normal (simple) graph production system. Any derivation results obtained by the tool (e.g. graphs that can be derived from the start graph or the actual rule applications) can be transformed back to multigraphs using the Sim−1 mapping. This forth and back translation can be used, for instance, for exchanging results between different graph transformation tools. 6 Conclusion and Future Work We have proposed a method for performing DPO multigraph transformations using tools han- dling SPO simple graph transformations. Compared to previous work [HKM06], this method is generic, i.e. has been proved correct on categorical level and does not depend on the tools to be used. Pushing theory to work in practise. Tool interoperability is one major motivating point to translate graph transformation systems using multigraphs and DPO to equivalent systems with simple graphs and SPO derivations. On the more fundamental level it is even more interesting to have the possibilities of applying a wide range of theoretical results and implementing them in the tool of favour. During the last three decades, a lot of theory was developed using DPO and multi- graphs. One special new technique is the analysis of derivations using Subobject Transformation Systems (STS) presented in [CHS06]. Since the GROOVE tool performs graph derivations to verify systems, the translation presented in this paper could give the possibility of combining the power of both (which was not possible before, because STS are not defined for SPO). And indeed, this idea already has a concrete structure: basically one can exploit the possible results of dependencies using a translation to STSs and furthermore, the branching derivations of the state space can be folded into one summary object. Thus, only a small number of derivation steps will have to be performed to construct an abstraction of a much bigger state space. The idea is then to use the abstraction equipped with an STS to deliver only effective states and perform model checking on these states and their concrete successors. Proc. GT-VMT 2007 12 / 14 ECEASST Acknowledgements. The first and third authors are employed in the GROOVE project funded by the Dutch NWO (project number 612.000.314). Bibliography [BW95] M. Barr, C. Wells. Category Theory for Computing Science. Prentice Hall, 1995. [CHS06] A. Corradini, F. Hermann, P. Sobociński. Subobject Transformation Systems. Ap- plied Categorical Structures, 2006. To appear. [CMR+97] A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel, M. Löwe. Algebraic Approaches to Graph Transformation, Part I: Basic Concepts and Double Pushout Approach. Pp. 163–246 in [Roz97]. [Cou97] B. Courcelle. The Expression of Graph Properties and Graph Transformations in Monadic Second-Order Logic. Pp. 313–400 in [Roz97]. [DKH97] F. Drewes, H.-J. Kreowski, A. Habel. Hyperedge Replacement Graph Grammars. Pp. 95–162 in [Roz97]. [EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. EATCS Monographs in TCS. Springer Verlag, 2006. [EHK+97] H. Ehrig, R. Heckel, M. Korff, M. Löwe, L. Ribeiro, A. Wagner, A. Corradini. Algebraic Approaches to Graph Transformation, Part II: Single Pushout Approach and Comparison with Double Pushout Approach. Pp. 247–312 in [Roz97]. [Hau06] J. H. Hausmann. Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Techniques. PhD thesis, Universität Paderborn, 2006. [HHT96] A. Habel, R. Heckel, G. Taentzer. Graph Grammars with Negative Application Con- ditions. Special issue of Fundamenta Informaticae 26(3,4):287–313, 1996. [HKM06] F. Hermann, H. Kastenberg, T. Modica. Towards Translating Graph Transformation Approaches by Model Transformation. In Proc. of the Int. Workshop on Graph and Model Transformation (GraMoT’06). 2006. [KKR06] H. Kastenberg, A. Kleppe, A. Rensink. Defining Object-Oriented Execution Seman- tics Using Graph Transformations. In Gorrieri and Wehrheim (eds.), Proc. of the 8th IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS’06). LNCS 4037, pp. 186–201. Springer Verlag, 2006. [Kön02] B. König. Hypergraph Construction and its Application to the Static Analysis of Concurrent Systems. Mathematical Structures in Computer Science 12(2):149–175, 2002. 13 / 14 Volume 6 (2007) Simulating Multigraph Transformations [LS04] S. Lack, P. Sobociński. Adhesive Categories. In Walukiewicz (ed.), Proc. of the 7th Int. Conf. on Foundations of Software Science and Computation Structures (FOS- SACS’04). LNCS 2987, pp. 273–288. Springer Verlag, 2004. [OMG05] OMG. Unified Modeling Language Specification. 2005. http://www.omg.org/technology/documents/formal/uml.htm [Ren04a] A. Rensink. The GROOVE Simulator: A Tool for State Space Generation. In Pfaltz et al. (eds.), Applications of Graph Transformations with Industrial Relevance (AG- TIVE’03). LNCS 3062, pp. 479–485. Springer Verlag, 2004. [Ren04b] A. Rensink. Representing First-Order Logic using Graphs. In Ehrig et al. (eds.), Proc. of the 2nd Int. Conf. on Graph Transformations (ICGT’04). LNCS 3256, pp. 319–335. Springer Verlag, 2004. [Roz97] G. Rozenberg (ed.). Handbook of Graph Grammars and Computing by Graph Transformation. Volume I: Foundations. World Scientific, 1997. [SSHW] A. Schürr, S. E. Sim, R. Holt, A. Winter. The GXL Graph eXchange Language. http://www.gupro.de/GXL [Tae01] G. Taentzer. Towards Common Exchange Formats for Graphs and Graph Transfor- mation Systems. In Padberg (ed.), Proc. of the Workshop on Uniform Approaches to Graphical Process Specification Techniques (UNIGRA’01). ENTCS 44. 2001. [TER99] G. Taentzer, C. Ermel, M. Rudolf. The AGG Approach: Language and Tool Envi- ronment. In Ehrig et al. (eds.), Handbook of Graph Grammars and Computing by Graph Transformations. Volume II: Applications, Languages and Tools, pp. 163– 246. World Scientific, 1999. Proc. GT-VMT 2007 14 / 14 http://www.omg.org/technology/documents/formal/uml.htm http://www.gupro.de/GXL Introduction Background Graphs and Graph Morphisms Graph Transformations Back to the Example From Multigraphs to Simple Graphs and back again From Multigraphs to Simple Graphs From Simple Graphs to Multigraphs Categories for Multigraphs and Simple Graphs Multigraph versus Simple Graph transformations Extensions Simulation in SPO Tools Conclusion and Future Work