Permutation Equivalence of DPO Derivations with Negative Application Conditions based on Subobject Transformation Systems Electronic Communications of the EASST Volume 16 (2009) Proceedings of the Doctoral Symposium at the International Conference on Graph Transformation (ICGT 2008) Permutation Equivalence of DPO Derivations with Negative Application Conditions based on Subobject Transformation Systems Frank Hermann 16 pages Guest Editors: Andrea Corradini, 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 Permutation Equivalence of DPO Derivations with Negative Application Conditions based on Subobject Transformation Systems Frank Hermann1 1 frank(at)cs.tu-berlin.de Institut für Softwaretechnik und Theoretische Informatik, TU Berlin, Germany Abstract: Switch equivalence for transformation systems has been successfully used in many domains for the analysis of concurrent behaviour. When using graph transformation as modelling framework for these systems, the concept of negative application conditions (NACs) is widely used – in particular for the specification of operational semantics. In this paper we show that switch equivalence can be improved essentially for the analysis of systems with NACs by our new concept of permutation equivalence. Two derivations respecting all NACs are called permutation-equivalent, if they are switch-equivalent disregarding the NACs. In fact, there are permutation-equivalent derivations which are not switch-equivalent with NACs. As main result of the paper, we solve the following problem: Given a derivation with NACs, we can efficiently derive all permutation-equivalent derivations to the given one by static analysis. The results are based on extended techniques for subobject transformation systems, which have been introduced recently. Keywords: Graph Transformation, Adhesive Categories, Subobject Transformation Systems, Negative Application Conditions, Process Analysis 1 Introduction Transformation systems based on the double pushout (DPO) approach [CMR+97] with negative application conditions (NACs) [HHT96, EEPT06] are a suitable modelling framework for sev- eral application domains, e.g. definition of operational semantics and simulation. In this context, the analysis of concurrent behaviour of an execution of the system is of interest. A process of an execution describes all possible equivalent executions. Correspondingly, a process of a deriva- tion defines an equivalence class of derivations. Processes of graph transformation systems based on the DPO approach [CMR96] were defined as occurrence grammars in [Bal00]. Occurrence grammars were lifted to the abstract setting of adhesive rewriting systems [BCH+06] in order to generalise the process construction. This opened possibilities for analysing processes of trans- formation systems based on arbitrary adhesive categories [LS04], such as typed graphs, graphs with scopes and graphs with second order edges. This paper extends the standard switch equivalence of derivations without and with nega- tive application conditions to the so-called permutation equivalence of derivations with nega- tive application conditions (NACs) in adhesive categories. The main difference is that there 1 / 16 Volume 16 (2009) mailto:frank(at)cs.tu-berlin.de Permutation Equivalence of DPO Derivations with Negative Application Conditions are permutation-equivalent derivations with NACs, which cannot be derived by switching NAC- independent neighbouring derivation steps. The challenge is to efficiently calculate derivations, which are equivalent in the sense that all NACs are respected and the matches of the original derivation are preserved. However, a direct construction of all permutation-equivalent deriva- tions is complex in general. First of all, the amount of possible permutations is high in general and furthermore, the permutations have to be derived from the original derivation by computing the new matches and the new intermediate objects from the old ones and checking that all NACs are fulfilled. The main result of this paper is a framework for the efficient analysis of permutation equiv- alence, i.e. the efficient construction of all derivations, which are permutation-equivalent to a given one (see Theorems 1 - 3 in Sec. 5). The presented technique is based on subobject trans- formation systems (STSs) [CHS08], which can be constructed in advance, i.e. possibly before a user requests an analysis. They are based on the process construction given in [BCH+06] and we extend them for the case with NACs. This builds the basis for efficient dependency checks between components of pairs of rule occurrences, where expensive pattern matching is avoided. The next section reviews transformation systems and introduces the new notion of permuta- tion equivalence. Thereafter, subobject transformation systems (STSs) as process model of a derivation are reviewed and Section 4 shows how the process construction can be extended to systems with NACs. Thereafter, Section 5 presents the analysis of permutation equivalence of derivations with NACs and shows as a main result that the analysis can be transferred to the de- rived STS leading to correct results for the original system. Section 6 concludes the main results and discusses future work within the presented framework. 2 Transformation Systems and Permutation Equivalence In this section we review transformation systems based on the double pushout (DPO) approach and the standard switch equivalence of derivations. We present an example in the context of workflow modelling, where we use negative application conditions (NACs) and show that switch equivalence does not lead to all intuitively equivalent derivations in our example. For this reason we introduce the new notion of permutation equivalence, which leads to the discussed equivalent derivations. A derivation in an adhesive category C is given by a sequence of rule applications within a grammar. A transformation rule p = (L ←l− K −r→ R) consists of three objects L, K, R ∈ Ob j(C) being left-hand side, interface, and a right-hand side, respectively, NAC q | EE ""E EE L m �� noo (PO1) K loo r // �� (PO2) R m∗�� G Doo // H and two monomorphisms l, r ∈ Mor(C). The interface K contains the part which is not changed by the rule and hence occurs in both L and R. Applying a rule p to an object G means to find a monomor- phism m : L → G and to replace the matched part in G by the corresponding right-hand side R of the rule, thus leading to a transformation step G p,m =⇒ H. In this paper, matches are required to be monomorphisms. But as explained in [HE08, Her09b], the analysis based on subobject transfor- mation systems is also possible for systems with non-monomorphic matching. A transformation step is given by a double-pushout (DPO), where D is the intermediate object after constructing the pushout complement for pushout (PO1) and in (PO2) H is constructed as gluing of D and R Proc. Doctoral Symposium ICGT 2008 2 / 16 ECEASST via K. A sequence of transformation steps d = (d1; . . . ; dn) is called a derivation. A rule may con- tain a set of negative application conditions (NACs) [HHT96, EEPT06]. A NAC (N, n : L → N) of a rule consists of a negative pattern N together with a monomorphism n from the left hand side of the rule to N. Intuitively, it forbids the presence of a certain pattern in an object G to which the rule shall be applied. A match L −m→ G satisfies a NAC n : L → N, written m |= N, if there is no monomorphism N −q→ G with q◦n = m. Typed transformations are based on a type object TG and the derived slice category C ↓ TG, where each object G is typed over TG by typeG : G → TG and morphisms are compatible with the typing morphisms. A grammar specifies a start object, a type graph and a set of rules for performing typed transformations. Definition 1 (Grammar) Given a category C, a grammar GG = (SG, TG, P, π) consists of a type object TG, a start object SG, a finite set of rule names P and a function π , which maps a rule name to a rule with NACs p = (p, N) containing a rule p = (L ←l− K −r→ R) and a finite set of negative application conditions N. The start graph and the productions of GG are typed over TG. TG worksOn Person Task started SG :Person :Task :Person L :worksOn 1:Person 2:Task :started K 1:Person 2:Task R 1:Person 2:Task :started NAC1 2:Task 1:Person startTask R :worksOn 1:Person 2:Task K 1:Person 2:Task L 1:Person 2:Task R :worksOn 1:Person 2:Task K 1:Person 2:Task L 1:Person 2:Task :started finishTask stopTask continueTask 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 NAC1 :worksOn :Person 2:Task 1:Person 3:started 3:started Figure 1: The graph grammar GG Example 1 (Graph Grammar GG) Figure 1 shows the graph grammar GG = (SG, TG, P, π) for mobile agents in reconfigurable networks. The mappings of the rule morphisms are specified by numbers. Rule “startTask” assigns a person to a task via an edge of the type “worksOn”, but the rule is not applicable if the task was already started, as specified by the NAC “NAC1”. Rule “finishTask” is inverse to “startTask” and removes the assignment and the edge of the type 3 / 16 Volume 16 (2009) Permutation Equivalence of DPO Derivations with Negative Application Conditions “started”, while rule “stopTask” also deletes the assignment, but not the flag “started”. Finally, rule “continueTask” specifies that a person may continue the work, which possibly was started by another person and stopped meanwhile. The NACs NAC1 and NAC2 of this rule require that neither the person itself nor another person is working on the task to be assigned. Switch equivalence of derivations without NACs is based on sequential independence. Definition 2 (Sequential Independence without NACs) Let d = (G0 = p1,m1===⇒ G1 = p2,m2===⇒ G2) be a derivation without NACs in a grammar GG. Then, d1 = G0 = p1,m1===⇒ G1 and d2 = G1 = p2,m2===⇒ G2 are two sequentially inde- pendent derivation steps, if there exist i : R1 → D2, j : L2 → D1 in the diagram on the right, which shows parts of the derivation diagrams, s.t. l′2 ◦i = m ′ 1 and r ′ 1 ◦ j = m2. K1 �� // R1 m′1 // ��/ / i "" L2 m2 �� ���� j || K2 �� oo D1 r′1 // G1 D2l′2oo Remark 1 (Local Church Rosser) Two sequentially independent derivation steps without NACs can be switched by the Local Church Rosser Theorem (Thm. 5.12 in [EEPT06]). By mk : Lk → G′k we denote the match for rule pk in the new order of the steps. Given a derivation without NACs, switch equivalence leads to the complete set of its equivalent derivations [BCH+06]. Note that DPO derivation diagrams are unique up to isomorphism only, thus we relate isomorphic derivation diagrams by “∼=” meaning that there are isomorphisms between the objects compatible with the involved morphisms. Definition 3 (Switch Equivalence without NACs) Let d = (d1; . . . ; dk; dk+1; . . . dn) be a deriva- tion without NACs in grammar GG, where dk; dk+1 are two sequentially independent derivation steps. Let d′ be derived from d by switching (dk; dk+1) to (d′k+1; d ′ k) according to the Local Church Rosser Theorem. Then, d′ is a switching of d, written d sw∼ d′. Switch-equivalence sw ≈ is the union of the transitive closure of sw∼ and the relation ∼= for isomorphic derivations. We now extend the notion of switch equivalence to derivations with NACs using sequential independence for derivations with NACs according to [HHT96, LEO06]. Definition 4 (Sequential Independence with NACs) Let d = (G0 = p1,m1===⇒ G1 = p2,m2===⇒ G2) be a derivation with NACs in a grammar GG. Suppose that i : R1 → D2, j : L2 → D1 exist in the two deriva- tion diagrams on the right, s.t. l′2◦i = m ′ 1, r ′ 1◦ j = m2. Suppose also that the derived match m1 : L1 → G′1 L1 m1 �� K1 �� //oo R1 m′1 // ��/ / i "" L2 m2 �� ���� j || K2 �� oo // R2 m′2 �� G0 D1 r′1 // l′1 oo G1 D2 l′2 oo r′2 // G2 by the Local Church Rosser Theorem and the match m2 = l′1 ◦ j : L2 → G0 fullfill all NACs, i.e. m2 |= N2 for each NAC (n2 : L2 → N2) of p2 and m1 |= N1 for each NAC (n1 : L1 → N1) of p1. Then, G0 = p1,m1===⇒ G1, G1 = p2,m2===⇒ G2 are two sequentially independent derivation steps with NACs. Definition 5 (Switch Equivalence with NACs) Let d = (d1; . . . ; dk; dk+1; . . . dn) be a derivation with NACs in grammar GG, where dk; dk+1 are two sequentially independent derivation steps with NACs. Let d′ be derived from d by switching dk; dk+1 to d′k+1; d ′ k according to the Local Proc. Doctoral Symposium ICGT 2008 4 / 16 ECEASST Church Rosser Theorem. Then, d′ is a switching with NACs of d, written d swN∼ d′. Switch equivalence with NACs swN ≈ is the union of the transitive closure of swN∼ and the relation ∼= for isomorphic derivations. G1 4:worksOn 1:Person 3:Task 6:started 2:Person ⇒ ⇒ ⇒ G0 1:Person 3:Task 6:started 2:Person G2 1:Person 3:Task 6:started 2:Person G3 5:worksOn 1:Person 3:Task 6:started 2:Person G4 1:Person 3:Task 6:started 2:Person ⇒ Figure 2: Derivation d in the grammar GG Example 2 (Derivation in GG) Derivation d = (d1; d2; d3; d4) = (G0 = continueTask,m1========⇒ G1 = stopTask,m2======⇒ G2 = continueTask,m3========⇒ G3 = stopTask,m4======⇒ G4) in Fig. 2 describes that at first person “1” works on task “3” and afterwards person “2” works on the same task, but both of them stop without finishing the task. Derivation steps d2 to d4 are dependent from their preceding steps and thus, no switching of independent steps is possible: the second step deletes edge “4” produced by the first step, the NAC of the third step forbids the presence of “4”, which is deleted by the second, and finally, the fourth step deletes edge “5” that was created by the third step. However, there is a permutation of the steps, which is conceptually equivalent to the depicted derivation. Consider d′ = (d′3; d ′ 4; d ′ 1; d ′ 2), where the third and fourth steps are moved to the front, all NACs are respected and the rules of GG are applied at the same places of the graph that is transformed. Since switch equivalence is not general enough for transformation systems with NACs as shown and explained in Example 2, we introduce the notion of permutation equivalence for derivations with NACs, which relates all equivalent derivations that respect the NACs. In partic- ular, the equivalent permutation of the example can be derived by the new notion. Definition 6 (Permutation Equivalence of Derivations) Two derivations d and d′ with NACs in a grammar GG are permutation-equivalent, written d π ≈ d′, if disregarding the NACs, they are switch-equivalent. A direct analysis of permutation equivalence in the adhesive category of the derivations is possible, but can be quite complex, if e.g. the graphs of the derivation are much bigger than in the simple running example. For each possible switching disregarding the NACs we have to update the derivation diagrams and perform pattern matching for the NACs on the updated objects in order to check whether the new derivation is permutation-equivalent. Therefore, we suggest to first construct a process model based on Subobject Transformation Systems, and then to perform a more efficient analysis on it. Accordingly, the main results of this paper, given by Theorems 1 - 3 in Sec. 5, show that the analysis on the basis of STSs is sound and complete and that the process model can be constructed efficiently. Next, we will show how subobject transformation systems can be used as process model for a derivation without NACs. Thereafter, we present in Sec. 4 how they can be extended to the case with NACs leading to an efficient analysis framework for permutation equivalence, which is shown and explained in Sec. 5. 5 / 16 Volume 16 (2009) Permutation Equivalence of DPO Derivations with Negative Application Conditions 3 Subobject Transformation Systems Processes of a graph grammar are defined as occurrence grammars together with a mapping to the original grammar. The concept of occurrence grammars was extended to the more abstract setting of adhesive rewriting systems [BCH+06] based on subobjects. This technique was fur- ther elaborated in [CHS08] introducing the general concept of subobject transformation systems (STSs). In this section we review STSs and their construction from a given derivation without NACs. A subobject A of an object T of a category C is an equivalence class of monomorphisms a : A → T . We write A for short to denote a representative of the equivalence class and we leave the monomorphism a implicit. The category of subobjects of T is called Sub(T ) and its morphisms f : A → B are those monomorphisms in C, which are compatible with the implicit monomorphisms to T , i.e. b◦ f = a for a : A → T and b : B → T . If such an f exists, we write A ⊆ B for short. Definition 7 (Subobject Transformation Systems) A Subobject Transformation System S = (S0, T, P, π) over an adhesive category C consists of a super object T ∈ C, a start object S0 ⊆ T in Sub(T ), a set of production names P, and a function π , which maps a production name q to a production 〈 Lq, Kq, Rq 〉 , where Lq, Kq, and Rq are objects in Sub(T ), Kq ⊆ Lq and Kq ⊆ Rq. The application of a production in an STS is based on union and intersection, which are co- product and product in category Sub(T ) and they can be constructed in the underlying adhesive category C as follows: A∩B is given by the pullback of A → T ← B and A∪B is given by the pushout of A ← A∩B → B. The implicit monomorphism of A∩B is given by A∩B → A → T and the one of A∪B is the induced one by the pushout property [LS04]. Definition 8 (Direct Derivations) Let S = (S0, T, P, π) be a Subobject Transformation System, π(q) = 〈L, K, R〉 be a production, and let G be an object of Sub(T ). Then there is a direct derivation from G to G′ using q, written G = q ⇒ G′, if G′ ∈ Sub(T ) and if there exists an object D ∈ Sub(T ) such that: (i) L∪D ∼= G; (ii) L∩D ∼= K; (iii) D∪R ∼= G′, and (iv) D∩R ∼= K. According to Proposition 6 of [CHS08] a direct derivation in an STS induces a DPO diagram in the underlying adhesive category C. Therefore, a derivation in an STS, specified by its sequence of rule names, gives rise to a derivation in C. Definition 9 (Derivation of an STS-sequence) Let dS = (G0 = q1=⇒ G1 =⇒ . . . = qn=⇒ Gn) be a deriva- tion in an STS S. Let s = 〈q1; . . . ; qn〉 be the sequence of the rule occurrences according to dS. Then, drv(s) denotes the sequence of DPO diagrams in C for each derivation Gi−1 = qi⇒ Gi in S. In order to derive all switch-equivalent derivations to a given one we can analyse its process, which is given by an isomorphism class of occurrence grammars together with a mapping to the original grammar as presented in [CMR96, BCH+06]. An occurrence grammar directly corresponds to an STS and in fact, the construction of an STS in [CHS08] from a given derivation tree coincides with the above construction of an occurrence grammar in the case of a linear derivation, i.e. there is a one-to-one correspondence between both representations. In analogy to Proc. Doctoral Symposium ICGT 2008 6 / 16 ECEASST [BCH+06], we explicitly define the start object S0 of an STS derived from a derivation instead of leaving it implicit. Furthermore, this paper does not consider general derivation trees, but derivation sequences, for which we extend the analysis to the case with NACs in Sec. 5. Definition 10 (STS of a Derivation) Let d = (G0 = q1,m1===⇒ . . . = qn,mn===⇒ Gn) be a derivation in an adhesive category. The derived STS of d is denoted by Prc(d) and constructed as follows: Prc(d) = (S0, T, P, π), where T is the colimit of the DPO-diagrams given by d, S0 is given by the embedding G0 ⊆ T , P = {(qi, i) | i ∈ [n]} is a set that contains a rule occurrence name for each rule occurrence in d and π maps each rule occurrence name (qi, i) to the rule occurrence at the i(th) step in d extended by the embeddings into T . The sequence of rule occurrence names of P according to d is denoted by seq(d). In [BCH+06] the set of all linearisations of the process is derived using compound relations, which can be obtained from basic relations as shown in [CHS08]. Hence, we can use the follow- ing general relation of independence subsuming the basic relations for analysing switch equiva- lence. Definition 11 (Independence of Productions in STSs) Let S = (S0, T, P, π) be an STS and let q1, q2 ∈ P be two production names, and π(pi) = 〈Li, Ki, Ri〉 for i ∈{1, 2} be the corresponding productions. Then, q1 and q2 are independent, denoted q1 ♦ q2, if (L1 ∪R1)∩(L2 ∪R2) ⊆ (K1 ∩K2). In the following, we define the switch equivalence for sequences of rule occurrence names within an STS, which will be used in Sec. 5 for the analysis of permutation equivalence. Definition 12 (Switch-Equivalence of Sequences) Let S = (S0, T, P, π) be an STS, let d be a derivation in S and let s = 〈q1, . . . , qn〉 be its corresponding sequence of rule occurrence names. Let qk,qk+1 be independent in S, then the sequence s′ = 〈q1, . . . , qk+1, qk, . . . , qn〉 is switch- equivalent to the sequence s, written s sw∼S s′. Switch equivalence sw ≈S of sequences is the transitive closure of sw∼S . 4 Subobject Transformation Systems with NACs In this section, we extend the definition of subobject transformation systems to STSs with NACs. Each rule in an STS is extended by an ordered list of NACs, which is later used by the dependency relations in Sec. 5 for specifying the NAC that is causing a dependency. Definition 13 (STS with NACs) A Subobject Transformation System with NACs S = (S0, T, P, π) over an adhesive category C consists of a super object T ∈ C, a start object S0 ⊆ T in Sub(T ), a set of production names P, and a function π , which maps a production name q to a production with NACs ( 〈 Lq, Kq, Rq 〉 , N), where Lq, Kq, and Rq are objects in Sub(T ), Kq ⊆ Lq, Kq ⊆ Rq and N is an ordered list of negative application conditions with L ⊆ N[i] ⊆ T , where N[i] denotes the i(th) element of N. 7 / 16 Volume 16 (2009) Permutation Equivalence of DPO Derivations with Negative Application Conditions Direct derivations with NACs in an STS correspond to direct derivations with NACs in the underlying adhesive category, but the check of a NAC to be found in the intermediate object G is simplified, because a NAC in an STS cannot occur at several positions in G. Definition 14 (Direct Derivations with NACs) Let S =〈S0, T, P, π〉 be a Subobject Transforma- tion System with NACs, π(q) = (〈L, K, R〉, N) be a production with NACs, and let G be an object of Sub(T ). Then there is a direct derivation with NACs from G to G′ using q, written G = q ⇒ G′, if G′ ∈ Sub(T ) and for each N[i] in N: N[i] * G and if there exists an object D ∈ Sub(T ) such that: (i) L∪D ∼= G; (ii) L∩D ∼= K; (iii) D∪R ∼= G′, and (iv) D∩R ∼= K. The extension of the process mapping Prc for derivations with NACs in an adhesive category is based on the following instantiation of NACs applied for all derivation steps. Definition 15 (Instantiated NACs) Let (Ni, ni)∈ N be a NAC of a rule p = (p, N) of a grammar GG = (SG, TG, P, π) in an adhesive category, with p = (L ←l− K −r→ R), let d be a derivation with NACs in GG, where p is applied at step k via the match mk, and let T be the colimit of the derivation diagram of d. An instantiated NAC M of (Ni, ni) is a subobject of T (M ⊆ T ), such that M ∼= Ni, L ⊆ M and M is compatible with the typing of Ni and with ni, i.e. typeNi = typeT ◦ incM,T ◦ isoM and incL,M = isoM ◦ni as shown on the right. The set of all instantiated NACs of p is denoted by NacsT (p, mk). Ni typeNi 00 isoM GG ##G G Loo nioo � _ �� l L zzvv vv vv(=) M �� // T typeT��(=) T G Remark 2 Note that given a NAC, then the set of its instantiated NACs may be empty, which means that the NAC cannot be found within T . Furthermore, a set of instantiated NACs may be infinite if T or d are infinite. In this case the analysis in Sec. 5 may not be decidable. However, in the case of finite derivation sequences and objects being finite in its structural part, e.g. finite graph structure of an attributed graph with an infinite algebra, we get a finite list for each NAC. Note further that (Ni, incM,T ◦isoM) ∼= (M, incM,T ) in Sub(T ). Definition 16 (Derived STS with NACs) Let GG be a grammar in an adhesive category C and let d = (G0 = p1,m1===⇒ . . . = pn,mn===⇒ Gn) be a derivation in GG. The STS for d is given by Prc(d) = (S0, T, P, π), where T is the colimit of the derivation diagram of d, S0 is given by G0 and its em- bedding to T , P is a set of rule names, each distinguished name qk corresponds to a derivation step dk = Gk−1 = pk,mk===⇒ Gk in d and the mapping π is given as follows: π(qk) = (〈Lk ⊇ Kk ⊆ Rk〉, Nk), where Nk is an ordered list of the set NacsT (qk, mk). The order of Nk is arbitrary but fixed. The sequence of rule names of P in d is denoted by seq(d). T 4:worksOn 1:Person 3:Task 6:started 2:Person 5:worksOn S0 1:Person 3:Task 6:started 2:Person Figure 3: Super object T and start object S0 of the STS Prc(d) Example 3 (STS of a Derivation) For the derivation d = (G0 = continueTask,m1========⇒ G1 = stopTask,m2======⇒ G2 Proc. Doctoral Symposium ICGT 2008 8 / 16 ECEASST cont1 L 4:worksOn 1:Person 6:started K 1:Person R 1:Person 3:Task N1[2] 5:worksOn 1:Person 3:Task 6:started 3:Task 6:started 3:Task R 5:worksOn 1:Person 3:Task K 1:Person 3:Task L 2:Person 3:Task N1[1] 4:worksOn 2:Person 3:Task 1:Person stop2 R 4:worksOn 1:Person 3:Task K 1:Person 3:Task L 1:Person 3:Task stop1 cont2 L 5:worksOn 2:Person 6:started K 2:Person R 2:Person 3:Task 6:started 3:Task 6:started 3:Task 6:started6:started N2[2] 5:worksOn 2:Person 3:Task N2[1] 4:worksOn 1:Person 3:Task 2:Person 6:started6:started Figure 4: Rule occurrences of the STS Prc(d) = continueTask,m3========⇒ G3 = stopTask,m4======⇒ G4) in Fig. 2 we construct the STS S = Prc(d) = (S0, T, P, π) as shown in Fig. 3 and Fig. 4, where numbers denote the embeddings to the colimit T of the derivation diagram. The start object S0 is given by G0 in d and its embedding to T . Rule occurrences “cont1” and “cont2” correspond to the first and third derivation step, respectively. Each NAC of “continueTask” can be instantiated once, given by N1[1] and N1[2] for “cont1”. For “cont2” they are instantiated to N2[1] and N2[2]. The rule occurrences “stop1” and “stop2” correspond to the second and forth derivation step of d. As explained before in Example 2, no switching is possible in d. 5 Efficient Analysis In order to analyse dependencies within the process Prc(d) of a derivation d with NACs two new relations are introduced specifying weak enabling and weak disabling dependencies. Here we can use the fact that the NACs in an STS are given as ordered lists to indicate the concrete NAC instantiation that is causing a dependency. These relations are used to characterise the permutation equivalence of derivations with NACs by properties in the derived STS shown by the main technical result of the paper in Thm. 1. Intuitively, q1 weakly enables q2 if it deletes an item that is part of the forbidden structure of the NAC N2[i] of q2. This means that there is an element in L1 ∩N2[i] that is not contained in K1 ∪L2. Analogously, q1 is weakly disabled by q2 if q2 produces an item that is part of the forbidden structure of the NAC N1[i] of q1. Definition 17 (Weak NAC Enabling) Let q1 and q2 be two rules in an STS and let N2[i] be a NAC of q2, i.e. N2[i] ∈ N2 for π(q2) = (〈L2, K2, R2〉, N2). The relation