key: cord-0046331-eenftvew authors: Lambers, Leen; Orejas, Fernando title: Initial Conflicts for Transformation Rules with Nested Application Conditions date: 2020-05-31 journal: Graph Transformation DOI: 10.1007/978-3-030-51372-6_7 sha: 06657738a971cf50e49e8ca3734c73dfd23b028c doc_id: 46331 cord_uid: eenftvew We extend the theory of initial conflicts in the framework of [Formula: see text]-adhesive categories to transformation rules with ACs. We first show that for rules with ACs, conflicts are in general neither inherited from a bigger context any more, nor is it possible to find a finite and complete subset of finite conflicts as illustrated for the category of graphs. We define initial conflicts to be special so-called symbolic transformation pairs, and show that they are minimally complete (and in the case of graphs also finite) in this symbolic way. We show that initial conflicts represent a proper subset of critical pairs again. We moreover demonstrate that (analogous to the case of rules without ACs) for each conflict a unique initial conflict exists representing it. We conclude with presenting a sufficient condition illustrating important special cases for rules with ACs, where we do not only have initial conflicts being complete in a symbolic way, but also find complete (and in the case of graphs also finite) subsets of conflicts in the classical sense. Detecting and analyzing conflicts is an important issue in software analysis and design, which has been addressed successfully using powerful techniques from graph transformation (see, e.g., [12, 15, 17, 24] ), most of them based on critical pair analysis. The power of critical pairs is a consequence of the fact that: a) they are complete, in the sense that they represent all conflicts; b) there is a finite number of them; and c) they can be computed statically. The main problem is that their computation has exponential complexity in the size of the preconditions of the rules. For this reason, some significantly smaller subsets of critical pairs that are still complete have been defined [1, 19, 21] , clearing the way for a more efficient computation. In particular, recently, in [19] , a new approach Subset of conflicts, complete [27] Subset of conflicts, complete [17, 20] Symbolic, complete [6, 9] Initial conflicts Subset of conflicts, min. complete, proper subset of CPs [1, 19] Symbolic (Definition 10), min. complete, regular (Theorem 6) & conservative extension of CPs (Theorem 7) Symbolic (Definition 10), min. complete, proper subset of CPs (Theorem 3) for conflict detection was introduced based on a different intuition. Instead of considering conflicts in a minimal context, as for critical pairs, we used the notion of initiality to characterize a complete set of minimal conflicts, showing that initial conflicts form a strict subset of critical pairs. In particular, we have that every conflict is represented by a unique initial conflict, as opposed to the fact that each conflict may be represented by many critical pairs. Most of the work on critical pairs only applies to plain graph transformation systems, i.e. transformation systems with unconditional rules. Nevertheless, in practice, we often need to limit the application of rules, defining some kind of application conditions (ACs). In this sense, in [17, 20] we defined critical pairs for rules with negative application conditions (NACs), and in [6, 9] for the general case of ACs, where conditions are as expressive as arbitrary first-order formulas on graphs. However, to our knowledge, no work has addressed up to now the problem of finding significantly smaller subsets of critical pairs for this kind of rules. In this paper we generalize the theory of initial conflicts to rules with ACs in the framework of M-adhesive transformation systems. In particular, the main contributions of this paper (as summarized in Table 1 ) are: -The definition of the notion of initial conflict for rules with ACs, based on a notion of symbolic transformation pair, showing that the set of initial conflicts is a proper subset of the set of critical pairs and that it is minimally complete 1 , in the sense that, no smaller set of symbolic transformation pairs exists that is also complete. In particular, the cardinality of the set of initial conflicts is, at most, the cardinality of the set of initial conflicts for the plain case, when disregarding the ACs, plus one. Moreover, as in the plain case, every conflict is an instance of a unique initial conflict. -The identification of a class of regular initial conflicts that demonstrate a certain kind of regularity in their application conditions. This allows us to unfold them into a complete (and in the case of graphs also finite) subset of conflicts. In particular, we show that, in the case of rules with NACs, initial conflicts are regular, implying that our initial conflicts represent a conservative extension of the critical pair theory for rules with NACs. The paper is organized as follows. We describe related work in Sect. 2 and, in Sect. 3, we present some preliminary material, where we also include some new results. More precisely, in Subsect. 3.1 and Subsect. 3.2 we briefly reintroduce the framework of M-adhesive categories and of rules with ACs; in Subsect. 3.3 we reintroduce critical pairs for rules with ACs following [6, 9] ; in Subsect. 3.4 we reintroduce initial conflicts for plain rules, and in Sect. 4 we introduce initial parallel independent transformation pairs. This result is used in Sect. 4, where we present the main results of the paper about initial conflicts for rules with ACs. Then, in Sect. 5 we show our results on unfolding initial conflicts. Finally, we conclude in Sect. 6 discussing some future work. Detailed proofs can be found in the full version of the paper [23] . Most work on checking confluence for rule-based rewriting systems is based on the seminal paper from Knuth and Bendix [14] , who reduced the problem of checking local confluence to checking the joinability of a finite set of critical pairs. This technique has been extensively studied in the area of term rewriting systems (see, e.g., [25] ), and it was introduced in the area of graph transformation by Plump [27] in the context of term-graph and hypergraph rewriting. Moreover, he also proved that (local) confluence of graph transformation systems is undecidable, even for terminating systems, as opposed to what happens in the area of term rewriting systems. However, recently, in [2] it is shown that confluence of terminating DPO transformation of graphs with interfaces is decidable. The authors explain that the reason is that interfaces play the same role as variables in term rewriting systems, where confluence is undecidable for terminating ground (i.e., without variables) systems, but decidable for non-ground ones. Computing critical pairs in graph transformation, as introduced by Plump [27] , is exponential in the size of the preconditions of the rules. For this reason, different proper subsets of critical pairs with a considerably reduced size were studied that are still complete [1, 19, 21] , clearing the way for a more efficient computation. The notion of essential critical pair [21] for graph transformation systems already allowed for a significant reduction, and, the notion of initial conflict [19] , introduced for the more general M-adhesive systems, allowed for an even larger reduction. However, not all M-adhesive categories have initial conflicts. In [19] it is shown that typed graphs do have them and [1] extended that result proving that arbitrary M-adhesive categories satisfying some given conditions also have initial conflicts. A recent line of work concentrates on the development of multi-granular conflict detection techniques [3, 18, 24] . An extensive literature survey shows [24] that conflict detection is used at different levels of granularity depending on its application field. The overview shows that conflict detection can be used for the analysis and design phase of software systems (e.g. for finding inconsistencies in requirement specifications), for model-driven engineering (e.g. supporting model version management), for testing (e.g. generation of interesting test cases), or for optimizing rule-based computations (e.g. avoiding backtracking). These multigranular techniques are presented for rules without application conditions (ACs). Our work builds further foundations for providing multi-granular techniques also in the case of rules with ACs in the future. The use of (negative) application conditions, to limit the application of graph transformation rules, was introduced in [8, 10] , while the more general approach, using nested conditions, was introduced by Habel and Penneman [11] . Checking confluence for graph transformation systems with application conditions (ACs) has been studied in [17, 20] for the case of negative application conditions (NACs), and in [6, 9] for the more general case of ACs. However, it is an open issue to find proper subsets of critical pairs of considerably reduced size in the general case. We start with a brief introduction of M-adhesive categories, rules with nested application conditions (ACs) (cf. Subsect. 3.2), and the main parts of critical pair theory for this type of rules [6, 9] (cf. Subsect. 3.3). Thereafter, we reintroduce the notion of initial conflicts [19] for plain rules, i.e. rules without ACs (cf. Subsect. 3.4). We also introduce the notion of initial parallel independent transformation pairs as a counterpart (cf. Subsect. 3.5), since it will play a particular role when defining initial conflicts for rules with ACs in Subsect. 3.4. We assume that the reader is acquainted with the basic theory of DPO graph transformation and, in particular, the standard definitions of typed graphs and typed graph morphisms (see, e.g., [5] ) and its associated category, Graphs T G . Our results do not only apply to a specific class of graph transformation systems, like standard (typed) graph transformation systems, but to systems over any M-adhesive category [5] . The idea behind considering M-adhesive categories is to avoid similar investigations for different instantiations like e.g. Petri nets or hypergraphs. An M-adhesive category is a category C with a distinguished morphism class M of monomorphisms satisfying certain properties. The most important one is the van Kampen (VK) property stating a certain kind of compatibility of pushouts and pullbacks along M-morphisms. Moreover, additional properties are needed in our context: initial pushouts, describing the existence of a special "smallest" pushout over a morphism, E -M pair factorizations, extending the classical epi-mono factorization to a pair of morphisms with the same codomain. The definitions of these properties can be found in [6, 7] . Remark 1. Most categories of structures used for specification are M-adhesive and satisfy these additional properties [5] , including the category Graphs T G , M with M being the class of all injective typed graph morphisms. Nested application conditions [11] (in short, application conditions, or just ACs) generalize the corresponding notions in [4, 10, 15] , where a negative (positive) application condition, short NAC (PAC), over a graph P , denoted ¬∃a (∃a) is defined in terms of a morphism a : P → C. Informally, a morphism m : P → G satisfies ¬∃a (∃a) if there does not exist a morphism q : C → G extending a to m (if there exists q extending a to m). Then, an AC is either the special condition true or a pair of the form ∃(a, ac C ) or ¬∃(a, ac C ), where ac C is an additional AC on C. Intuitively, a morphism m : P → G satisfies ∃(a, ac C ) if m satisfies a and the corresponding extension q satisfies ac C . Moreover, ACs may be combined with the usual logical connectors. For a concrete definition of ACs we address the reader to [11] or [6] . ACs are used to restrict the application of rules to a given object. The idea is to equip the precondition (or left hand side) of rules with an application condition. Then we can only apply a given rule to an object G if the corresponding match morphism satisfies the AC of the rule. However, for technical reasons, we also introduce the application of rules disregarding the associated ACs. A rule ρ = p, ac L consists of a plain rule p = L ← I → R with I → L and I → R morphisms in M and an application condition ac L over L. (1) and (2), called DPO, with match m and comatch m * such that m |= ac L . (1) and (2), where m does not necessarily need to satisfy ac L . Given a set of rules R for C, M , the triple C, M, R is an M-adhesive system. In the rest of the paper we assume that each rule (resp. transformation or M-adhesive system) comes with ACs. Otherwise, we state that we have a plain rule (resp. transformation or M-adhesive system), which can be seen as a special case, in the sense that the ACs are (equivalent to) true. ACs can be shifted over morphisms and rules as shown in the following lemma (for constructions see [7] 2 and [7, 11] , respectively). [7] ). There is a transformation Shift from morphisms and ACs to ACs such that for each AC, ac P , and each morphism b : P → P , Shift transforms ac P via b into an AC Shift(b, ac P ) over P such that for each morphism n : P → H it holds that n • b |= ac P ⇔ n |= Shift(b, ac P ). Lemma 2 (shift ACs over rules [7, 11] ). There is a transformation L from rules and ACs to ACs such that for every rule ρ : L ← I → R and every AC on For parallel independence, when working with rules with ACs, we need not only that each rule does not delete any element which is part of the match of the other rule, but also that the resulting transformation defined by each rule application still satisfies the ACs of the other rule application. A transformation pair is in conflict or conflicting if it is parallel dependent. We distinguish different conflict types, generalizing straightforwardly the conflict characterization introduced for rules with NACs [20] . The transformation pair H 1 ⇐ ρ1,o1 G ⇒ ρ2,o2 H 2 is a use-delete (resp. delete-use) conflict if in Definition 2 the commuting morphism d 12 (resp. d 21 ) does not exist, i.e. the second (resp. first) rule deletes something used by the first (resp. second) one. Moreover, it is an AC-produce (resp. produce-AC ) conflict if in Definition 2 the commuting morphism d 12 (resp. d 21 ) exists, but an extended match is produced by the second (resp. first) rule that does not satisfy the rule AC of the first (resp. second) rule. If a transformation pair is an AC-produce or produce-AC conflict, then we also say that it is an AC conflict or AC conflicting. A use-delete (resp. delete-use) conflict cannot occur simultaneously to an AC-produce (resp. produce-AC) conflict, since the AC of the first (resp. second) rule can only be violated iff there exists an extended match for the first (resp. second) rule. However, a use-delete (resp. delete-use) conflict may occur simultaneously to a produce-AC (resp. ACproduce) conflict. For grasping the notion of completeness of transformation pairs w.r.t. a property like parallel (in-)dependence, it is first important to understand how a given transformation can be extended to another transformation. In particular, an extension diagram describes how a transformation t : G 0 ⇒ * G n can be extended to a transformation t : G 0 ⇒ * G n via the same rules and an extension morphism k 0 : G 0 → G 0 that maps G 0 to G 0 as shown in the following diagram on the left. For each rule application and transformation step, we have two double pushout diagrams as shown on the right, where the rule ρ i+1 is applied to G i and G i . We introduce two notions of completeness, distinguishing M-completeness from regular completeness, depending on the membership of the extension morphism in M. It is known that critical pairs (resp. initial conflicts) for plain rules are M-complete (resp. complete) w.r.t. parallel dependence [5, 19] . In Subsect. 3.3, we reintroduce the fact that critical pairs for rules with ACs are M-complete w.r.t. parallel dependence, but as symbolic transformation pairs. We learn in Sect. 4 that initial conflicts for rules with ACs are also complete in this symbolic way. ρ 1 , ρ 2 is complete (resp. M- complete) w.r.t. parallel (in-)dependence if there is a pair P 1 ⇐ ρ1,o1 K ⇒ ρ2,o2 P 2 from S and an extension diagram via extension morphism m (resp. m ∈ M) for each parallel (in-)dependent direct transformation pair H 1 ⇐ ρ1,m1 G ⇒ ρ2,m2 H 2 . K P1 P2 G H1 H2 m ρ1, o1 ρ2, o2 ρ1, m1 ρ2, m2 Critical pairs for plain rules are just transformation pairs, where morphisms o 1 and o 2 are in E (i.e., roughly, K is an overlapping of L 1 and L 2 ). In the category of Graphs they lead to finite and complete subsets of finite conflicts [4] (assumed that the rule graphs are also finite). However, when rules include ACs, we cannot use the same notion of critical pair since, as we show in Theorem 2, in general, for any two rules with ACs, there is no complete set of transformation pairs that is finite. To avoid this problem, our critical pairs for rules with ACs also include ACs, as in [6, 9] , where they are proved to be M-complete, and they are also finite in the category of Graphs (assumed again that the rules are finite). In particular, critical pairs are based on the notion of symbolic transformation pairs, which are pairs of AC-disregarding transformations on some object K with two special ACs on K. These two ACs, ac K (extension AC ) and ac * K (conflict-inducing AC ), are used to characterize which embeddings of this pair, via some morphism m : K → G, give rise to a transformation pair that is parallel dependent. If m |= ac K , then m • o 1 : L 1 → G and m • o 2 : L 2 → G are two morphisms, satisfying the associated ACs of ρ 1 and ρ 2 , respectively. Moreover, if m |= ac * K , then the two transformations H 1 ⇐ ρ1,m•o1 G ⇒ ρ2,m•o2 H 2 are parallel dependent. Symbolic transformation pairs allow us to present critical pairs as well as initial conflicts (cf. Subsect. 3.4) in a compact and unified way, since they both are instances of symbolic transformation pairs. Finally, note that each symbolic transformation pair stp K : tp K , ac K , ac * K is by definition uniquely determined (up to isomorphism and equivalence of the extension AC and conflictinducing AC) by its underlying AC-disregarding transformation pair. Given rules ρ 1 = p 1 , ac L1 and ρ 2 = p 2 , ac L2 , a symbolic transformation pair stp K : tp K , ac K , ac * K for ρ 1 , ρ 2 consists of a pair tp K : P 1 ⇐ ρ1,o1 K ⇒ ρ2,o2 P 2 of AC-disregarding transformations together with ACs ac K and ac * K on K given by: ac L2 ) , called extension AC, and ac * K = ¬(ac * K,d12 ∧ ac * K,d21 ), called conflict-inducing AC with ac * K,d12 and ac * K,d21 given as follows: → P 2 are defined by the corresponding double pushouts. A critical pair is now a symbolic transformation pair in a minimal context such that there exists at least one extension to a pair of transformations being parallel dependent. Definition 6 ((M-)completeness of symbolic transformation pairs) . A set of symbolic transformation pairs S for a pair of rules ρ 1 , ρ 2 is complete (resp. M-complete) w.r.t. parallel dependence if there is a symbolic transformation pair stp K : tp K : P 1 ⇐ ρ1,o1 K ⇒ ρ2,o2 P 2 , ac K , ac * K from S and an extension diagram as depicted in Fig. 1 with In [6, 9] it is shown that the set of critical pairs for a pair of rules is Mcomplete w.r.t. parallel dependence. Initial conflicts for plain rules follow an alternative approach to the original idea of critical pairs. Instead of considering all conflicting transformations in a minimal context (materialized by a pair of jointly epimorphic matches), initial conflicts use the notion of initiality of transformation pairs to obtain a more declarative view on the minimal context of critical pairs. Each initial conflict is a critical pair but not the other way round. Moreover, all initial conflicts for plain rules are complete w.r.t. parallel dependence and they still satisfy the Local Confluence Theorem for plain rules. Consequently, initial conflicts for plain rules represent an important, proper subset of critical pairs for performing static conflict detection as well as local confluence analysis. (1) and (2) and extension morphism f I , as in the left diagram below, such that for each transformation pair tp : H 1 ⇐ p1,m 1 G ⇒ p2,m 2 H 2 that Given a plain M-adhesive system with initial transformation pairs for conflicts, an initial conflict is a conflict tp isomorphic to tp I . The idea of representing all conflicts by a (finite) set of initial conflicts is based on the requirement of the existence of initial transformation pairs for parallel dependent or conflicting plain transformation pairs. This requirement holds for the category of typed graphs [19] and for any arbitrary M-adhesive category fulfilling some extra conditions [1] . For plain M-adhesive systems, initial conflicts are critical pairs [19] . Moreover, they are complete and minimal as transformation pairs w.r.t. parallel dependence, whereas critical pairs for plain rules are M-complete [4] . In this section, we show the existence of initial transformation pairs for parallel independent transformation pairs (Fig. 2) , allowing us to define a complete subset also w.r.t. parallel independence. The proof requires that binary coproducts exist. Uniqueness of initial transformation pairs up to isomorphism implies that for each pair of plain rules p 1 , p 2 there is a unique initial parallel independent transformation pair tp L1+L2 : : H 1 ⇐ p1,m1 G ⇒ p2,m2 H 2 is an initial parallel independent transformation pair if it is isomorphic to the transformation pair tp L1+L2 : : H 1 ⇐ p1,m1 G ⇒ p2,m2 H 2 , then tp L1+L2 : R 1 + L 2 ⇐ p1,i1 L 1 +L 2 ⇒ p2,i2 L 1 +R 2 ,R 1 + L 2 ⇐ p1,i1 L 1 + L 2 ⇒ p2,i2 L 1 + R 2 . The one-element set consisting of the initial parallel independent transformation pair for a given pair of rules is complete w.r.t. parallel independence. L1+L2 : R 1 + L 2 ⇐ p1,i1 L 1 + L 2 ⇒ p2,i2 L 1 + R 2 for a pair of plain rules p 1 , p 2 is complete w.r.t. parallel independence. We start with showing why it is not possible to straightforwardly generalize the idea of initial conflicts from plain rules to rules with ACs. On the one hand, conflict inheritance, which was the basis for showing completeness of initial conflicts for plain rules, does not hold any more. Moreover, it is impossible in general to find a finite and complete subset of finite conflicts for rules with ACs Conflicts are in general not inherited (as opposed to the case of plain rules [19] ), i.e., not each (initial) transformation pair that can be embedded into a conflicting one will be conflicting again. This may happen in particular for AC conflicts. Use-delete (resp. delete-use) conflicts for rules with ACs are still inherited. tp is also in use-delete (resp. delete-use) conflict. ← → (with AC true), producing an outgoing edge with a node, and p 2 : ← → with NAC ¬∃n : → , producing a node only if two other nodes do not exist already. Consider graph G = , holding two nodes. Applying both rules to G (with the matches sharing one node in G) we obtain a produce-AC conflict since the first rule creates a third node, forbidden by the second rule. Now both rules can be applied similarly to the shared node in the subgraph G = of G obtaining parallel independent transformations, illustrating that AC-conflicts are not inherited. We show that in M-adhesive categories, in particular in the category of graphs, it is in general impossible to find a finite and complete subset of conflicts for finite rules with ACs. If it would always exist, we could derive that each first-order formula is equivalent to a finite disjunction of atomic formulas. Theorem 2. Given finite rules ρ 1 = p 1 , ac L1 and ρ 2 = p 2 , ac L2 for the M-adhesive category Graphs, in general, there is no finite set of finite transformation pairs S for ρ 1 and ρ 2 that is complete w.r.t. parallel dependence. We generalize the notion of initial conflicts for plain rules to rules with ACs. In particular, we introduce them as special symbolic transformation pairs. They are conflict-inducing meaning that there needs to exist an unfolding of the symbolic transformation pair into a concrete conflicting transformation pair. Moreover, their AC-disregarding transformation pair needs to be an initial conflict or initial parallel independent transformation pair. We also show the relationship between initial conflicts and critical pairs as reintroduced in Subsect. 3.3, demonstrating that initial conflicts represent a proper subset of critical pairs. Definition 9 (unfolding of symbolic transformation pair). Given a symbolic transformation pair stp K : tp K , ac K , ac * K for rule pair ρ 1 , ρ 2 , then its unfolding U(stp K ) consists of all transformation pairs H 1 ⇐ ρ1,m1 G ⇒ ρ2,m2 H 2 representing the lower row of the extension diagrams via some extension morphism m : K → G as shown in Fig. 1 (with AC-disregarding transformation pair tp K in the upper row). Moreover, we say that stp K is conflict-inducing if its unfolding includes a conflicting transformation pair. Consider an M-adhesive system with initial transformation pairs for conflicts along plain rules. An initial conflict for rules ρ 1 = p 1 , ac L1 and ρ 2 = p 2 , ac L2 is a conflict-inducing symbolic transformation pair stp K : tp K , ac K , ac * K with the AC-disregarding transformation pair tp K being initial, i.e. either tp K is an initial conflict for rules p 1 and p 2 (in this case stp K is called a use-delete/delete-use initial conflict) or it is the initial parallel independent transformation pair tp L1+L2 for rules p 1 and p 2 (in this case stp K = stp L1+L2 = tp L1+L2 , ac L1+L2 , ac * L1+L2 is called the AC initial conflict). Note that the unfolding of a conflict-inducing symbolic transformation pair (and in particular of an AC initial conflict) may also include parallel independent transformation pairs. All conflicts in the unfolding of an AC initial conflict are AC conflicts, and never use-delete/delete-use conflicts (because otherwise we would get a contradiction using Lemma 4). Example 2 (initial conflict). Consider again the rules from Example 1. Applying both rules to L 1 + L 2 = (with disjoint matches) we obtain the AC initial conflict stp K = stp L1+L2 = tp L1+L2 , ac L1+L2 , ac * L1+L2 . Thereby ac L1+L2 is equivalent to ¬∃( ), expressing that when during extension both nodes are merged, no two additional nodes, otherwise not one additional node should be given. Moreover, ac * L1+L2 is equivalent to ∃( ), expressing that either both nodes are not merged during extension, otherwise one additional node should be present for a conflict to arise. Both transformation pairs (the conflicting one from G = as well as the parallel independent one from its subgraph G = , sharing the merged node in their matches) described in Example 1 belong to its unfolding. Each initial conflict is in particular also a critical pair. The reverse direction of Theorem 3 does not hold. In general, critical pairs stp K : tp K , ac K , ac * K where tp K represents a use-delete/delete-use conflict (but is not initial yet) are represented by the initial conflict stp I : tp I , ac I , ac * I with tp I the unique initial conflict for tp K as plain transformation pair. Moreover, critical pairs stp K : tp K , ac K , ac * K where tp K is parallel independent as plain transformation pair are represented by one initial conflict stp L1+L2 : tp L1+L2 , ac L1+L2 , ac * L1+L2 with tp L1+L2 the initial parallel independent transformation pair. Consider again the rules from Example 1 and their application to G = . The symbolic transformation pair stp G : tp G , ac G , ac * G is a critical pair, but not an initial conflict. We show that initial conflicts are complete (not M-complete as in the case of critical pairs) w.r.t. parallel dependence as symbolic transformation pairs. Consider an M-adhesive system with initial transformation pairs for conflicts along plain rules. The set of initial conflicts for a pair of rules ρ 1 , ρ 2 is complete w.r.t. parallel dependence. For each conflict a unique (up-toisomorphism) initial conflict exists representing it, since this property is inherited from the one for plain rules [19] and the fact that the initial parallel independent pair of transformations is unique w.r.t. a given rule pair. Initial conflicts are also minimally complete, i.e. we are able to generalize the corresponding result for plain rules to rules with ACs. We show a sufficient condition for being able to unfold initial conflicts into a complete set of conflicts that is finite if the set of initial conflicts is finite (cf. Subsect. 5.1). We demonstrate moreover that this sufficient condition is fulfilled for the special case of having merely NACs as rule application conditions (cf. Subsect. 5.2). Finally, we show that in this case we obtain in particular specific critical pairs for rules with negative application conditions (NACs) as introduced in [20] again. In this sense we show explicitly that initial conflicts as introduced in this paper represent a conservative extension of the critical pair theory for rules with NACs. We introduce regular initial conflicts leading to M-complete subsets of conflicts by unfolding them in some particular way (cf. disjunctive unfolding in Definition 11). The idea is that the extension and conflict-inducing AC (ac K and ac * K , respectively) of such a conflict stp K : tp K , ac K , ac * K have a specific form that is amenable to finding M-complete unfoldings. We expect the condition ac K ∧ ac * K to consist of a disjunction of positive literals (conditions of the form ∃(a i : K → C i , c i )) with a negative remainder (i.e. a condition c i = ∧ j∈J ¬∃(b j : C i → C j , d j )). Intuitively, this means that there is a finite number of possibilities to unfold the symbolic conflict into a concrete conflict by adding some specific positive context (expressed by the morphism a i ). The negative remainder c i ensures that by adding this positive context to the context K of the symbolic transformation pair within the initial conflict, we indeed find a concrete conflict when not extending further at all. Moreover, it expresses under which condition the corresponding concrete representative conflict leads to further conflicts by extension. Finally, the subsets of M-complete conflicts built using the disjunctive unfolding are finite if the set of initial conflicts it is derived from is finite. Consider an M-adhesive system with initial transformation pairs for conflicts along plain rules. Given an initial conflict stp K : tp K , ac K , ac * K for rules ρ 1 , ρ 2 , then we say that it is regular if ac K ∧ ac * K is equivalent to a condition ∨ i∈I ∃(a i : non-isomorphic and I some non-empty index set. Given a regular initial con- Remark 5 (disjunctive unfolding). The disjunctive unfolding of a regular conflict is non-empty, but might consist of less elements than literals in the disjunction ∨ i∈I ∃(a i : K → C i , c i ): if a morphism a i does not satisfy the gluing condition of the derived spans, then also every extension morphism starting from there will not satisfy the gluing condition, and we can safely ignore that case from the disjunctive unfolding. Consider an M-adhesive system with initial transformation pairs for conflicts along plain rules. Given a rule pair ρ 1 , ρ 2 with set S of initial conflicts such that each initial conflict stp in S is regular, then It is possible to automatically check if some initial conflict is regular by using dedicated automated reasoning [22] as well as symbolic model generation for ACs [28] as follows. The reasoning mechanism [22] is shown to be refutationally complete ensuring that if the condition ac K ∧ ac * K of some initial conflict is unsatisfiable, this will be detected eventually. Moreover, the related symbolic model generation mechanism [28] is able to automatically transform each condition ac K ∧ ac * K into some disjunction ∨ i∈I ∃(a i : K → C i , c i ) with c i a negative remainder if such an equivalence holds. We show that for rules with NACs initial conflicts are regular. This means that in this special case there exists a complete subset of conflicts that is finite (in the case of graphs and assuming finite rules). This conforms to the findings in [17, 20] , where an M-complete set of critical pairs -as specific subset of conflicts -for graph transformation rules with NACs was introduced [20] (and generalized to M-adhesive transformation systems [17] ). Consider an M-adhesive system with initial transformation pairs for conflicts along plain rules. Given some initial conflict stp K : tp K , ac K , ac * K for a pair of rules ρ 1 , ρ 2 with ac Li = ∧ j∈J ¬∃n j : L i → N j for i = 1, 2 and J some finite index set, then it is regular. In particular, ac K ∧ ac * K is equivalent to a condition ∨ i∈I ∃(a i : K → C i , c i ) with c i = ∧ q∈Q ¬∃n q a condition on C i and I some non-empty index set. The negative remainder c i of each literal in ∨ i∈I ∃(a i : K → C i , c i ) of a regular initial conflict for rules with NACs thus consists of a set of NACs. Intuitively this means that we obtain for each initial conflict an M-complete subset of concrete conflicts by adding the context described by a i . As long as no NAC from c i is violated we can extend such a concrete conflict to further ones. Consider an Madhesive system, with initial transformation pairs for conflicts along plain rules. Given a rule pair ρ 1 , ρ 2 with ac Li = ∧ j∈J ¬∃n j : L i → N j for i = 1, 2, then We show moreover that the initial conflict definition is a conservative extension of the critical pair definition for rules with NACs as given in [17, 20] , i.e., we show that each conflict in the disjunctive unfolding of an initial conflict as chosen in the proof of Theorem 6 is a critical pair for rules with NACs. In an M-adhesive system with initial transformation pairs for conflicts along plain rules, if stp K : tp K , ac K , ac * K is an initial conflict for rules ρ 1 , ρ 2 with ac Li = ∧ j∈J ¬∃n j : L i → N j for i = 1, 2 and J some finite index set, then each conflict as chosen in the proof of Theorem 6 in U D (stp) is in particular a critical pair for ρ 1 , ρ 2 as given in [17, 20] . Example 4 (conservative unfolding). Consider again the rules from Example 1 (having only NACs as ACs) and their application to the graph G = . The corresponding transformation pair tp G is a critical pair for rules with NACs as given in [17, 20] . This is because it is in particular a conflicting pair of transformations, and the morphism violating the NAC (since finding the three nodes) and therefore causing the conflict after applying the first rule to G = obtaining some graph H 1 = is jointly surjective together with the corresponding co-match. As argued already in Example 2 this critical pair for rules with NACs belongs to the unfolding (and in particular to the disjunctive unfolding) of the unique AC initial conflict stp L1+L2 : tp L1+L2 , ac L1+L2 , ac * L1+L2 . In this paper we have generalized the theory of initial conflicts (from plain rules, i.e. rules without application conditions) to rules with application conditions (ACs) in the framework of M-adhesive transformation systems. We build on the notion of symbolic transformation pairs, since it turns out that it is not possible to find a complete subset of concrete conflicting transformation pairs in the case of rules with ACs. We have shown that initial conflicts are (minimally) complete w.r.t. parallel dependence as symbolic transformation pairs. Moreover, initial conflicts represent (analogous to the case of plain rules) proper subsets of critical pairs in the sense that for each critical pair (or also for each conflict), there exists a unique initial conflict representing it. We concluded the paper by showing sufficient conditions for finding unfoldings of initial conflicts that lead to (finite and) complete subsets of conflicts (as in the case of rules with NACs). Thereby we have shown that initial conflicts for rules with ACs represent a conservative extension of the critical pair theory for rules with NACs. As future work we aim at finding further interesting classes allowing finite and (minimally) complete unfoldings into subsets of conflicts. This will serve as a guideline to be able to develop and implement efficient conflict detection techniques for rules with (specific) ACs, which has been an open challenge until today. We are moreover planning to develop (semi-)automated detection of unfoldings of initial conflicts of rules with arbitrary ACs using dedicated automated reasoning and model finding for graph conditions [22, 26, 28] . It would be interesting to investigate in which use cases initial conflicts (or critical pairs) are useful already as symbolic transformation pairs, and in which use cases we rather need to consider unfoldings indeed. This is in line with the research on multi-granular conflict detection [3, 18, 24] investigating different levels of granularity that can be interesting from the point of view of applying conflict detection to different use cases. Finally, we plan to investigate conflict detection in the light of initial conflict theory for attributed graph transformation [5, 13, 16] , and in particular the case of rules with so-called attribute conditions more specifically. It would also be interesting to further investigate initial conflicts for transformation rules (with ACs) not following the DPO approach. On the essence and initiality of conflicts in m-adhesive transformation systems Confluence of graph rewriting with interfaces Granularity of conflicts and dependencies in graph transformation systems Theory of constraints and application conditions: from graphs to high-level structures Fundamentals of Algebraic Graph Transformation M-adhesive transformation systems with nested application conditions. Part 2: embedding, critical pairs and local confluence M-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation Graph grammars with application conditions Local confluence for rules with nested application conditions Graph grammars with negative application conditions Correctness of high-level transformation systems relative to nested conditions Detection of conflicting functional requirements in a use case-driven approach: a static analysis technique based on graph transformation Attributed graph transformation via rule schemata: Church-Rosser theorem Simple word problems in universal algebras Graph-based specification of access control policies Improved conflict detection for graph transformation with attributes Certifying rule-based models using graph transformation Granularity of conflicts and dependencies in graph transformation systems: a two-dimensional approach Initial conflicts and dependencies: critical pairs revisited Conflict detection for graph transformation with negative application conditions Efficient conflict detection in graph transformation systems by essential critical pairs Tableau-based reasoning for graph properties Initial conflicts for transformation rules with nested application conditions Multi-granular conflict and dependency analysis in software engineering based on graph transformation Advanced Topics in Term Rewriting Development of correct graph transformation systems Hypergraph rewriting: Critical pairs and undecidability of confluence Symbolic model generation for graph properties We thank Jens Kosiol for pointing out that the set of initial conflicts for plain rules is not only complete, but also minimally complete. We were able to transfer this result to rules with ACs in this paper. Many thanks also to the reviewers for their detailed and constructive comments helping to finalize the paper.