Efficient Analysis of Permutation Equivalence of Graph Derivations Based on Petri Nets Electronic Communications of the EASST Volume 29 (2010) Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010) Efficient Analysis of Permutation Equivalence of Graph Derivations Based on Petri Nets Frank Hermann , Andrea Corradini , Hartmut Ehrig , Barbara König 14 pages Guest Editors: Jochen Küster, Emilio Tuosto 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 Efficient Analysis of Permutation Equivalence of Graph Derivations Based on Petri Nets Frank Hermann 1, Andrea Corradini 2, Hartmut Ehrig 1, Barbara König 3 1 [frank,ehrig]@cs.tu-berlin.de, Institut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin, Germany 2 andrea(at)di.unipi.it, Dipartimento di Informatica, Università di Pisa, Italy 3 barbara koenig(at)uni-due.de, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen, Germany Abstract: In the framework of graph transformation systems with Negative Ap- plication Conditions (NACs) the classical notion of switch equivalence of deriva- tions is extended to permutation equivalence, because there are intuitively equiva- lent derivations which are not switch-equivalent if NACs are considered. By def- inition, two derivations are permutation-equivalent, if they respect the NACs and disregarding the NACs they are switch equivalent. A direct analysis of permutation equivalence is very complex in general, thus we propose a much more efficient anal- ysis technique. For this purpose, we construct a Place/Transition Petri net, called dependency net, which encodes the dependencies among rule applications of the derivation, including the inhibiting effects of the NACs. The analysis of permutation equivalence is important for analysing simulation runs within development environments for systems modelled by graph transformation. The application of the technique is demonstrated by a graph transformation system within the context of workflow modelling. We show the effectiveness of the ap- proach by comparing the minimal costs of a direct analysis with the costs of the efficient analysis applied to a derivation of our example system. Keywords: graph transformation, Petri nets, process analysis, adhesive categories 1 Introduction Given a workflow of a system, it is often interesting to know whether the workflow can be im- proved, by executing the tasks in a different order, which might be more convenient for the user or preferable from an efficiency point of view. If the workflow is modelled by a Petri net, representing a deterministic process, these questions can be fairly easily answered: processes incorporate a notion of concurrency that can be exploited to rearrange the tasks, while still re- specting causality. In this paper we consider workflow models with two further dimensions, which consider- ably complicate the problem: first, we work in the general setting of (weak) adhesive categories [LS05, EEPT06] where we can model systems with an evolving topology, such as (attributed) graph transformation systems, in contrast to systems with a static structure. For the sake of con- 1 / 14 Volume 29 (2010) mailto:[frank,ehrig]@cs.tu-berlin.de mailto:andrea(at)di.unipi.it mailto:barbara_koenig(at)uni-due.de Analysis of Permutation Equivalence ciseness, the definitions and results in this paper are presented for graph transformation systems, and we refer to the companion technical report [HCEK10] for the general notions based on adhe- sive categories. As a second dimension, we take into account Negative Application Conditions (NACs) that are used to ensure the “absence” of forbidden structures when executing a transfor- mation step: NACs significantly improve the specification formalisms based on transformation rules leading to more compact and concise models as well as increased usability and as a matter of fact they are widely used in non-trivial applications. The presence of NACs leads to more complex interdependencies of tasks. For this reason, we introduce a notion of permutation equivalence on derivations with NACs, which is coarser and more adequate than the switch equivalence in the double-pushout (DPO) approach including NACs. As defined in [Her09] two derivations are called permutation- equivalent, if they respect the NACs and disregarding the NACs they are switch-equivalent. Using the notion of switch equivalence with NACs directly does not lead to all permutation- equivalent derivations of a given derivation in general. The main remaining problem is how to derive the complete set of all permutation-equivalent derivations to a given one. For this purpose, we construct a subobject transformation system (STS) via a standard colimit construction and from this STS we construct a dependency net, given by a standard P/T Petri net, which includes a complete account of the inhibiting effects of the NACs. The main result shows that complete firing sequences of this net are one-to-one with derivations that are permutation-equivalent to the given derivation, allowing us to derive the complete set of permutation-equivalent derivations. Finally, for a given derivation of a simple example system with NACs, we perform a detailed complexity analysis of the cost of identifying all permutation equivalent derivations using the reduction to a Petri net and its reachability graph, and compare it with a lower bound of the costs for a direct analysis, i.e. for computing all shift-equivalent derivations first, and then filtering out the ones which do not respect the NACs. We obtain a significant improvement in speed, which shows that the proposed technique can be efficient for many applications which involve the gen- eration of permutation-equivalent derivations. Furthermore, the constructed P/T Petri net can be used to derive specific permutations without generating the complete set first. In the context of workflow analysis, both goals are of central interest for the modelling of a system. The structure of the paper is as follows. Sec. 2 reviews the main concepts of permutation equivalence for graph transformation systems. The construction of the dependency net is pre- sented in Sec. 3 and in our main result it is shown to be sound and complete for computing the set of permutation-equivalent derivations. Sec. 4 validates the efficiency of the analysis based on an extended version of the running example. Finally, Sec. 5 sums up the main results, discusses related work, and points out aspects of future work. 2 Permutation Equivalence In this section we review the standard switch equivalence and the recently introduced permuta- tion equivalence [Her09] for graph transformation systems based on the double pushout (DPO) approach. The running example of this paper illustrates that there are derivations which are intuitively equivalent and also permutation-equivalent but not switch-equivalent. Proc. GT-VMT 2010 2 / 14 ECEASST Definition 1 (Graph Transformation System with NACs) A rule p = (Lp ←l− Kp −r→ Rp) is a pair of injective graph morphisms. A Negative Application Condition (NAC) for a rule p is an injective graph morphism n : Lp ↪→ N, having the left-hand side of p as source. A rule with NACs is a pair 〈p, N〉 where p is a rule and N = {ni : Lp ↪→ Ni}i∈I is a fi- nite set of NACs for p. A match of a rule p in a graph G is an injective graph mor- phism1 m : Lp ↪→ G; match m satisfies the NAC n : Lp ↪→ N for p, written m |= n, if there is no arrow g : N → G such that g ◦ n = m.2 We say that there is a direct derivation G = p,m =⇒ H from an object G to H using a rule with NACs 〈p, N〉 and a match m : Lp →G, if there are two pushouts (1) and (2) in Graphs, as depicted. A derivation respects the NACs, if m |= n for each NAC (n : Lp ↪→N)∈N. A typed graph transformation N / III $$I II Lp noo m �� (1) Kp �� r //loo (2) Rp �� G D //oo H system (GTS) with NACs is a tuple G = 〈Q, πN〉 where Q is a set of rule names, and πN maps each name q ∈ Q to a rule with NACs πN (q) = 〈 π(q), Nq 〉 in the category GraphsTG of graphs typed over a given type graph TG. A derivation (respecting NACs) of G is a sequence G0 = q1,m1===⇒ G1 ···= qn,mn===⇒ Gn, where q1, . . . , qn ∈Q and di = Gi−1 = π(qi),mi ====⇒ Gi are direct derivations (respecting NACs) for i∈1, . . . , n. Sometimes we denote a derivation as a sequence d = d1; . . . ; dn of direct derivations. worksOn member connectedTo device Person name: String accessLevel: Int Task name: String description: String acessLevel: Int AccessPoint IP: String Subnet: String started MobileDevice IP: String task Team name: String continueTask (NACs are not depicted) L :worksOn K R 3:started member task 2:Task accessLevel=lv 1:Person acessLevel=lv 2:Team 3:started member task 2:Task accessLevel=lv 1:Person acessLevel=lv 2:Team 3:started member task 2:Task accessLevel=lv 1:Person acessLevel=lv 2:Team Attributed Type Graph TG* Figure 1: Part of attributed transformation system GS∗, modeling mobile adhoc networks Example 1 (Graph Transformation System with NACs) Fig. 1 shows a part of an attributed graph grammar for modelling a workflow system in mobile adhoc networks, where persons can be assigned to teams and tasks and they can change their location implying that their mobile communication devices may need to reconnect to new access points. In order to simplify the further constructions we will use the reduced version of this grammar in Fig. 2. The type graph TG shows that nodes in the system represent either persons or tasks: a task is active if it has a 1 In the general case NAC-morphisms (n : L → N) and matches are not required to be injective. For the general case, our technique can be extended by the results in [HE08]. 2 Intuitively, the image of Lp in G cannot be extended to an image of the “forbidden context” N. 3 / 14 Volume 29 (2010) Analysis of Permutation Equivalence continueTask (short: “cont“) L :worksOn 1:Person 3:started K 1:Person R 1:Person 2:Task NAC2 :worksOn 1:Person 2:Task 3:started 2:Task 3:started 2:Task R :worksOn 1:Person 2:Task K 1:Person 2:Task L 1:Person 2:Task NAC1 :worksOn :Person 2:Task 1:Person stopTask (short: “stop“) 3:started 3:started :worksOn :started TG Person Task Type Graph Figure 2: Reduced transformation system GS as running example “:started” loop, and it can be assigned to a person with a “:worksOn” edge. Rule “stopTask” cancels the assignment of a task to a person; rule “continueTask” instead assigns the task, and it has two NACs to ensure that the task is not assigned to a person already. Fig. 3 shows two derivations respecting NACs of GS. In derivation d the only task is first continued by “1:Person”, and then, after being stopped, by “2:Person”. In d′ the roles of the two Persons are inverted. G1 w1:worksOn 1:Person 3:Task 4:started 2:Person G0 1:Person 3:Task 4:started 2:Person G2 1:Person 3:Task 4:started 2:Person G3 w2:worksOn 1:Person 3:Task 4:started 2:Person G4 1:Person 3:Task 4:started 2:Person G’1 w1:worksOn 1:Person 3:Task 4:started 2:Person G0 1:Person 3:Task 4:started 2:Person G’2 1:Person 3:Task 4:started 2:Person G’3 w2:worksOn 1:Person 3:Task 4:started 2:Person G4 1:Person 3:Task 4:started 2:Person cont,m1 ⇒ stop,m2 ⇒ stop,m4 ⇒ cont,m3 ⇒ cont,m1 ⇒ stop,m4 ⇒ stop,m2 ⇒ cont,m3 ⇒ ’ ’ ’’ d: d’: Figure 3: Derivation d (respecting NACs) of GS and permutation-equivalent derivation d′ The classical theory of the DPO approach (without NACs) introduces an equivalence among derivations which relates derivations that differ only in the order in which independent direct derivations are performed (see [Kre86, BCH+06]). The switch equivalence is based on the notion of sequential independence and on the Local Church-Rosser theorem. This is briefly summarised in the next definition. Definition 2 (Switch Equivalence on Derivations) Let d1 = G0 = p1,m1===⇒ G1 and d2 = G1 = p2,m2===⇒ G2 be two direct derivations. Then they are se- quentially independent if there exist arrows i : R1 → D2 and j : L2 →D1 such that l′2◦i = m ′ 1 and r ′ 1◦ j = m2 (see the diagram on the right, which shows part of the derivation diagrams). If d1 K1 �� // R1 m′1 // ��/ / i "" L2 m2 �� ���� j || K2 �� oo D1 r′1 // G1 D2l′2oo and d2 are sequentially independent, then according to the Local Church Rosser Theorem (Thm. 5.12 in [EEPT06]) they can be “switched” obtaining direct derivations d′2 = G0 = p2,m2===⇒ G′1 and d′1 = G ′ 1 = p1,m1===⇒ G2, which apply the two rules in the opposite order. Now, let d = (d1; . . . ; dk; dk+1; . . . ; dn) be a derivation, where dk and dk+1 are two sequentially independent direct derivations, and let d′ be obtained from d by switching them according to Proc. GT-VMT 2010 4 / 14 ECEASST the Local Church Rosser Theorem. Then, d′ is a switching of d, written d sw∼ d′. The switch equivalence, denoted sw ≈, is the smallest equivalence on derivations containing both sw∼ and the relation ∼= for isomorphic derivations. Corresponding notions of parallel and sequential independence have been proposed for graph transformation systems with NACs [HHT96, LEO06]. However, the derived notion of switch equivalence does not identify all intuitively equivalent derivations. The reason is that, in presence of NACs, there might be an equivalent permutation of the direct derivations that cannot be derived by switch equivalence. Looking at d in Fig. 3 there is no pair of consecutive direct derivations which is sequentially independent if NACs are considered. However, the derivation d′ should be considered as equivalent. There are also examples in which even the switching of blocks of several steps would not lead to all permutation-equivalent derivations. This brings us to the following, quite natural notion of permutation equivalence of derivations respecting NACs, first proposed in [Her09]. Note that for permutation-equivalent derivations d π ≈ d′ the sequence of rules used in d′ is a permutation of those used in d. Definition 3 (Permutation Equivalence of Derivations) Two derivations d and d′ respecting NACs are permutation equivalent, written d π ≈ d′ if, disregarding the NACs, they are switch equivalent as for Def. 2. 3 Dependency Net of a Derivation In order to efficiently analyse permutation equivalence of derivations we introduce the construc- tion of the dependency net of a given derivation with NACs. This Place/Transition Petri net purely encodes the dependencies between the derivation steps. The reachability graph of this net with initial marking determines the class of derivations which are permutation-equivalent to a given one. The construction of the dependency net is based on the construction of the subobject trans- formation sytem (STS) of a given derivation d according to [CHS08] and its extension to NACs in [Her09]. Subobjects of a graph G form the category of subobjects Sub(G), which contains subgraphs of G3 as objects and injective graph morphisms m : G1 → G2 between subgraphs as morphisms, where m is required to respect the injective embeddings of G1 and G2 to G. We will write G1 ∩G2 for the componentwise intersection and G1 ∪G2 for the componentwise union of subgraphs of G, where items are identified with respect to the injective embeddings of G1 and G2 into G. In order to construct the STS for a derivation d = (d1; . . . ; dn) we compute the colimit T of the se- quence of DPO diagrams, where all morphisms are injective. Thus, all objects and morphisms of this di- agram are in the category Sub(T ). The NACs of the rules do not occur in this diagram. Lk �� Kkoo // �� Rk �� G0 ++WWW WWWW WWWW WWWW W . . .oo // Gk−1 ##H HH H Dkoo // �� Gk }}{{{ { . . .oo // Gn tthhhh hhhh hhhh hh T 3 More formally, a subgraph is given by an equivalence class of injective graph morphisms to G, such that the image of all morphism is equal. 5 / 14 Volume 29 (2010) Analysis of Permutation Equivalence Definition 4 (STS of a derivation) A subobject transformation system S = 〈T, Q, π〉 consists of a super object T , a set of rule names Q, and a function π , which maps a name q ∈ Q to a rule, i.e., to a triple π(q) = 〈 Lq, Kq, Rq 〉 of subobjects of T such that Kq = Lq ∩Rq. Now, let G = 〈Q, π〉 be a graph transformation system, and let d = (G0 = q1,m1===⇒ . . . = qn,mn===⇒ Gn) be a derivation of G. The STS generated from d is defined as STS(d) = 〈T, P, π̂〉, where T is the colimit object of the diagram underlying the derivation d, P = {k | dk = (Gk−1 = qk,mk==⇒ Gk) is a step of d}, and π̂(k) = 〈Lk, Kk, Rk〉, where qk = (Lk ← Kk → Rk). For the rest of the paper, we consider only derivations such that the colimit T is a finite object, i.e. Sub(T ) is a finite lattice. This is guaranteed if each rule of G has finite left- and right-hand sides, and if the start object of the derivation is finite. The generation of an STS with NACs from a given derivation works as in Definition 4, but additionally each rule will be equipped with a list of NACs, i.e., those obtained as “instances” of the original NACs in the colimit object T . Note that one original NAC can have several instances, but also not a single one. Definition 5 (Instantiated NACs) Let d = d1; . . . ; dk; . . . ; dn be a derivation respecting NACs and let T be the colimit object of the derivation. Let 〈p, N〉 be the rule with NACs used in direct derivation dk and let NACS(p) = {n : Lp ↪→ N | n ∈ N}. The set of all instantiated NACs in T of the NACs of a rule p is given by NACST (p) = {N −tN−→ T in Sub(T ) | n ∈ N, s.t. tN ◦n = tL} for Lp −tL→ T in Sub(T ). Definition 6 (STS of a Derivation with NACs) Let G be a GTS with NACs and let d be a derivation of G respecting NACs. The STS with NACs generated by d is given by STSN (d) = 〈T, P, π̂N〉, where T and P are as in Def. 4, π̂N (k) = 〈π̂(k), Nk〉, π̂(k) is as in Def. 4, and Nk is an arbitrary but fixed linearisation of the instantiated NACs NACST (pk) as in Def. 5, where pk is the rule of G used in dk. q1=cont1 L w1:worksOn 1:Person 4:started K 1:Person R 1:Person 3:Task N1[2] w2:worksOn 2:Person 3:Task 4:started 3:Task 4:started 3:Task R w2:worksOn 1:Person 3:Task K 1:Person 3:Task L 2:Person 3:Task N1[1] w1:worksOn 1:Person 3:Task 1:Person q4=stop2 R w1:worksOn 1:Person 3:Task K 1:Person 3:Task L 1:Person 3:Task q2=stop1 q3=cont2 L w2:worksOn 2:Person 4:started K 2:Person R 2:Person 3:Task 4:started 3:Task 4:started 3:Task 4:started4:started N3[2] w2:worksOn 2:Person 3:Task N3[1] w1:worksOn 1:Person 3:Task 2:Person 4:started4:started T w1:worksOn 1:Person 3:Task 4:started 2:Person w2:worksOn Super Object Figure 4: Derived Subobject Transformation System STSN (d) Proc. GT-VMT 2010 6 / 14 ECEASST Example 2 (Derived STS STSN (d)) For the derivation d in Ex. 1 we derive the STS as shown in Fig. 4. The super object T is derived by taking the first graph of the derivation and adding the items, which are created during the transformation, i.e. the two edges of type “worksOn”. The derivation d involves the rules “continueTask” and “stopTask” and thus, the derived STS contains the rule occurrences “1 , cont1”, “2 , stop1”, “3 , cont2” and “4 , stop2”, where the NACs of the rule “continueTask” are instantiated. The following relations between the rules of an STS with NACs specify the possible depen- dencies among them: the first four relations are discussed in [CHS08], while the last two are introduced in [Her09]. In our case the STS with NACs is generated from a derivation d accord- ing to Def. 6. Definition 7 (Relations on Rules) Let q1 and q2 be two rules in an STS with NACs S = (T, P, πN ) with πN (q j) = ( 〈 L j, K j, R j 〉 , N j) for j ∈{1, 2} and N j = (N j[i])i=1..n j . The relations on rules are defined on P as follows: Name Notation Condition Read Causality q1