# Constructing Constraint-Preserving Interaction Schemes
in Adhesive Categories

Jens Kosiol, Lars Fritsche, Nebras Nassar, Andy Schürr, Gabriele Taentzer

► To cite this version:

Jens Kosiol, Lars Fritsche, Nebras Nassar, Andy Schürr, Gabriele Taentzer. Constructing Constraint-Preserving Interaction Schemes in Adhesive Categories. 24th International Workshop on Algebraic Development Techniques (WADT), Jul 2018, Egham, United Kingdom. pp.139-153, 10.1007/978-3-030-23220-7_8. hal-02364576

HAL Id: hal-02364576

https://inria.hal.science/hal-02364576

Submitted on 15 Nov 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Constructing Constraint-Preserving Interaction
Schemes in Adhesive Categories

Jens Kosiol¹[0000-0003-4733-2777], Lars Fritsche²[0000-0003-4996-4639], Nebras
Nassar¹[0000-0002-0838-6513], Andy Schürr²[0000-0001-8100-1109], and Gabriele
Taentzer¹[0000-0002-3975-5238]

¹ Philipps-Universität Marburg, Germany

{kosiolje,nassarn,taentzer}@mathematik.uni-marburg.de

² TU Darmstadt, Germany

{lars.fritsche,andy.schuerr}@es.tu-darmstadt.de

**Abstract.** When using graph transformations to formalize model trans-
formations, it is often desirable to design transformations that preserve
consistency with respect to a given set of (model) integrity constraints.
The standard approach is to equip transformations with suitable appli-
cation conditions such that the introduction of constraint violations is
prevented. This may lead to rules that are applicable seldom or even inap-
plicable at all, though. To supplement this approach, we present a new and
systematic procedure to develop correct-by-construction transformations
with respect to a special kind of constraints. Instead of controlling the
applicability of a rule we complement its action in such a way that a given
constraint holds after application: For every way in which the rule could
introduce a violation of the constraint, we derive a supplementary action
for the rule that remedies that violation. We formalize this construction
in the setting of adhesive categories for monotonic rules and positive
atomic constraints and present sufficient conditions for its correctness.

**Keywords:** Algebraic Graph Transformation · Interaction Scheme · Graph Constraints · Correctness-by-Construction · Adhesive Categories

# 1 Introduction

Algebraic graph transformation [4] has proved to be a suitable formal framework
to reason about model transformations [3]. In application scenarios like model
generation and editing or refactoring of models, it is desirable that transforma-
tions preserve consistency with respect to a set of integrity constraints. Nested
constraints [7] allow to express first-order properties of graphs and a large subset
of constraints formulated in OCL [17] – a widespread constraint language in
modeling – may be translated into those [18,14]. In the context of algebraic
graph transformation, the standard approach to ensure the validity of results
of transformations with respect to a constraint is to equip transformation rules
with suitable application conditions. This approach is elaborated for arbitrarily
nested constraints in *M*-adhesive categories [7] and has tool support for EMF
model transformations [14]. It comes in two variants: Given a constraint *c* and a rule, one can construct a *c-guaranteeing* and a *c-preserving* application condition for the rule. The *c-guaranteeing* application condition ensures that the rules' application is possible if and only if the constraint *c* is fulfilled afterwards. The *c-preserving* one is logically weaker: The constraint *c* is only ensured to be fulfilled after a rule application if it already was before. Though sound from the formal point of view for every constraint, from the practical point of view the results are especially satisfactory in the case of *negative* constraints, which forbid a certain structure to exist. Then the new application conditions prohibit applications of the rule that would introduce this structure. However, for *positive* constraints requiring structures to exist, an application of a rule may be prohibited, e.g., because it creates a structure that necessitates another structure to exist that is not created likewise. In this way, frequently the application conditions stemming from positive constraints lead to rules which are applicable only rarely or are even inapplicable at all (see Sect. 2 for a concrete example).

To supplement the approach described above, we develop an alternative construction. Given a positive constraint *c*, instead of using application conditions, our idea is to *complement the action of a rule* in such a way that *c* holds after its application. Our construction works for *monotonic rules*, i.e., rules which only create structure, and *positive atomic constraints*. Some instance *G* satisfies a positive atomic constraint – which may be compactly notated as $\forall (P, \exists C)$ where *P* is a subobject of *C* – if for all subobjects of *G* that are isomorphic to *P* there exists a subobject isomorphic to *C* which includes the image of *P*. Positive atomic constraints are highly relevant in practice, e.g., they occur frequently when translating OCL into graph constraints and the application conditions arising from them in the standard approach are often far too restrictive. The crucial idea of our approach is to calculate all possible ways in which the application of a rule *r* may lead to a new match for the *premise P* of a constraint $c = \forall (P, \exists C)$. These are the different ways in which an application of *r* may introduce a new violation of *c*. They can significantly differ from each other and thus require diverging actions to resolve the would-be introduced violation. Hence, for each such situation we derive a rule that includes *r* as subrule but additionally creates structure that complements the new match for *P* to a new match for *C*. All these rules are collected into an *interaction scheme* [6] that is *constraint-preserving*: Applying an interaction scheme means to apply a common subrule – here *r* – once and every other rule from the interaction scheme as often as possible but with fixed partial match given by the match of the common subrule (the common actions are only performed once). In this way, every image of *P* that gets newly created by an application of *r* is complemented to an image of *C* by application of one of the rules of the interaction scheme and the validity of the constraint is preserved. Slightly extending this construction also gives a *constraint-guaranteeing interaction scheme*, i.e., an interaction scheme that additionally includes rules that “repair” already existing violations.

The original motivation for this research is to continue work from [13]. There, multi-rules for triple graph grammars (TGGs) [20] – a formalism for the declar-
ative description of consistency relationships between two modeling languages with graph-like representations – have been developed. The exemplary multi-rules in [13] serve to preserve consistency with (informally described) constraints but were developed “by hand”. This has the disadvantage that preservation of the constraint is not ensured by construction and has to be checked on a case-by-case basis. Our work paves the way to automate the design of those multi-rules in a way that guarantees correctness by construction. Our restriction to monotonic rules corresponds to that motivation since TGGs are composed of those.

The main contribution of this paper is the introduction and formalization of constraint-preserving and -guaranteeing interaction schemes in the setting of adhesive categories [12]. It is organized as follows. In Sect. 2 we illustrate our results with an example. Section 3 recalls relevant background. In Sect. 4 we present our construction of interaction schemes while Sect. 5 points out further possibilities to refine that construction. Section 6 compares to related work before we conclude in Sect. 7. An extended version of this paper [11] includes all proofs.

## 2 Introductory Example

We adapt the example from [13] since, in a way, we continue the work of constructing multi-amalgamated rules for triple-graph grammars (TGGs). There, a TGG for co-evolution of a class diagram and a documentation structure is given. We use a simplified version of this example, namely a plain graph grammar.

The meta-model in Fig. 1 is a blueprint for simple documentation structures. They consist of Docs owning Entries. Moreover, Docs reference Docs and Entries. Figure 2 presents a grammar allowing to create instances of the meta-model. Black elements have to exist for a rule to be applicable and green elements (additionally marked with ++) are newly created upon

application. The rules allow for creation of a new Doc, creation of an Entry to an existing Doc, and insertion of the references, respectively.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Meta-model for documentation structures</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2. Monotonic rules to create documentation structures</figcaption></figure>

If an instance of that meta-model is to be understood as documentation structure for a class-diagram, it is reasonable, e.g., to expect owned Entries of referenced Docs to be referenced, too. This constraint is expressible as a positive atomic constraint. Figure 3 depicts it in an intuitive graphical representation.

The (simplified) constraint-preserving version of *createEntry* with respect to *PropagationOfEntries* is depicted in Fig. 4. Its application is prohibited at every
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Constraint *PropagationOfEntries*</figcaption></figure>

Doc that is already referenced by another one. Thus, the creatable instances and the order of possible rule applications are severely restricted. As an alternative, we will automatically derive so-called multi-rules like *createEntry-multi* depicted in Fig. 5. Applying it as a so-called *interaction scheme* with kernel rule *createEntry* at a Doc still creates an Entry but additionally inserts a reference to this Entry from every Doc that references the chosen Doc. This is equivalent to applying its complement rule (Fig. 6) at every possible match with fixed partial match induced by a precedent application of *createEntry*. Applying, e.g., the rule *createEntry* at

<figure><img src="image_5.png" /><figcaption>**Fig. 4.** Rule *createEntry-NAC* with *negative application condition* (the crossed-out red elements are forbidden to exist)</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>**Fig. 5.** Multi-rule of *createEntry* (when seen as interaction scheme, the parts decided by *createEntry* as subrule orated with a Kleene star are applied as often as possible)</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>**Fig. 6.** Complement rule of *createEntry-multi* for *createEntry* as subrule</figcaption></figure>

node d1 to the graph depicted in Fig. 7 leads to the graph in Fig. 8. This clearly violates the constraint *PropagationOfEntries*. While the rule *createEntry-NAC* is not applicable at that match, applying the rule *createEntry-multi* at it as interaction scheme leads to the valid instance depicted in Fig. 9.

<figure><img src="image_8.png" /><figcaption>**Fig. 7.** Example for an instance graph</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>**Fig. 8.** After application of rule *createEntry* at d1</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>**Fig. 9.** After application of *createEntry-multi* at d1</figcaption></figure>
## 3 Preliminaries

In this section, we present some technical preliminaries. We conduct our work in the framework of adhesive categories [12]. They have been introduced as a general setting for double pushout rewriting and can be understood as categories where pushouts along monomorphisms behave like pushouts along injective functions in the category of sets and functions. Here, we only recall rules and transformations in adhesive categories with a focus on multi-amalgamation after introducing positive atomic constraints.

To express properties of graphs in a way fitting to the algebraic approach to graph transformation, first graph predicates or graph conditions have been developed (being expressively equivalent to a first-order logic on graphs) and later been generalized to the setting of so-called *M*-adhesive categories [19,7]. Our approach deals with a small but nonetheless in practice highly important fragment of that logic, namely *positive atomic constraints* [4].

**Definition 1 (Positive atomic constraint).** In an adhesive category *C*, a positive atomic constraint *c* is a monomorphism *p* : *P* ↪→ *C* between two objects. We will write *c* = ∀ (*P*,∃*p* : *P* ↪→ *C*) or ∀ (*P*,∃*C*) for short for such a constraint. We call *P* the premise and *C* the conclusion of the constraint.

An object *G* satisfies a positive atomic constraint *c*, denoted by $G \models c$, if for every monomorphism $g : P \hookrightarrow G$ there exists a monomorphism $q : C \hookrightarrow G$ such that $g = q \circ p$.

Positive atomic constraints are the only kind of constraints we consider, so we will just call them constraints when this is not apt to introduce misunderstanding.

Rules are a declarative way to define transformations of objects. They consist of a left-hand side *L*, a right-hand side *R*, and an interface *K*. Informally, in the category of graphs, the application of a rule to a graph *G* means to delete the elements of *L* and create those of *R* while preserving the elements stemming from the interface *K*. A match identifies the “location” in *G* where this is done. Formally and more generally in adhesive categories, a transformation can be defined using two pushout diagrams.

**Definition 2 ((Monotonic) Rule. Transformation).** Given an adhesive category *C*, a rule *p* consists of three objects *L*, *K*, and *R*, called left-hand side (LHS), interface, and right-hand side (RHS), and two monomorphisms *l* : *K* ↪→ *L*, *r* : *K* ↪→ *R*. Its inverse rule is the rule $p^{-1} = (R \hookrightarrow K \hookrightarrow L)$. A rule *p* = (*L* ↪→ *K* ↪→ *R*) is called monotonic (or non-deleting) if *l* : *K* ↪→ *L* is an isomorphism. In that case we just write *r* : *L* ↪→ *R*.

Given a rule $p = (L \leftrightarrow K \leftrightarrow R)$, an object $G$, and a monomorphism $m : L \to G$, called match, a (direct) transformation $G \Rightarrow_{p,m} H$ from $G$ to $H$ via $p$ at match $m$ is defined by the diagram to the right where both squares are pushouts.

<figure><img src="image_11.png" /></figure>

A rule *p* is called applicable at match *m* if the first pushout square above exists, i.e., if $m \circ l$ has a pushout complement.
Since we exclusively consider monotonic rules in this paper, we will just call them rules and give the following definition for the monotonic case only. *Subrules* and their *multi-rules* have a twofold purpose. First, the application of a rule, then called a multi-rule, may be equivalently split into the application of a subrule followed by one of a *complement rule* with respect to that subrule. The construction of such a complement rule is not unique; a quite involved one can be found in [6]. For a simpler one for monotonic rules, also used in [13], we refer to the extended version of this paper [11]. An example is displayed in Fig. 6. This decomposition of a rule application allows for important extensions in two directions: coordinated parallelism and a for-each like syntax. A subrule may capture the common behavior of several multi-rules and thus serve as a kernel to amalgamate their respective actions into application of a single *multi-amalgamated* rule. Secondly, often a subrule is intended to be applied once followed by as many applications of the complement rule as possible. *Interaction schemes* unify both ideas into one concept: An interaction scheme consists of a bundle of multi-rules for the same *kernel rule*. Its application is defined by applying the kernel rule once and each of the complement rules of the multi-rules as often as possible with the fixed partial match given by application of the kernel rule.

**Definition 3 (Subrule. Multi-rule. Interaction scheme. Application).**

A subrule or kernel rule $r_0$ of a rule $r_1: L_1 \hookrightarrow R_1$ is a rule $r_0: L_0 \hookrightarrow R_0$ with kernel morphism $s_1: r_0 \hookrightarrow r_1$ consisting of the monic components $s_{1,L}: L_0 \hookrightarrow L_1$ and $s_{1,R}: R_0 \hookrightarrow R_1$ such that the arising square in the diagram to the right is a pullback. The rule $r_1$ is then called a multi-rule for $r_0$.

$$ 
\begin{array}{ccc}
L_0 & \xrightarrow{r_0} & R_0 \\
\bigwedge_{s_{1,L}} & & \bigwedge_{s_{1,R}} \\
L_1 & \xrightarrow{r_1} & R_1
\end{array}
$$

An interaction scheme is a finite set $ias = \{s_1, \dots, s_n\}$ of kernel morphism from a kernel rule $r_0$ to different multi-rules $r_1: L_1 \hookrightarrow R_1, \dots, r_n: L_n \hookrightarrow R_n$ of $r_0$. The application of the interaction scheme $ias$ to an object $G$ with kernel match $m_0: L_0 \hookrightarrow G$ is defined as follows: A maximal matching $J$ for $ias$ is computed, i.e., a family of matches $(m_j: L_j \hookrightarrow G)_{j \in J}$ with $L_j \in \{L_1, \dots, L_n\}$ for all $j \in J$ that is (i) consistent, i.e.,

$$ m_0 = m_j \circ s_{j,L} \text{ for all } j \in J $$

and (ii) maximal, i.e., no further match for one of the LHSs $L_1, \dots, L_n$ can be added to the family of matches such that it still is consistent.

Then, the (multi-)amalgamated rule $r_s: L_s \hookrightarrow R_s$, that is the rule arising by computing the colimits $L_s$ of the family of morphisms $(s_{j,L})_{j \in J}$ and $R_s$ of the family of morphisms $(s_{j,R})_{j \in J}$ with $r_s$ being induced by the universal property of $L_s$, is applied.

**Remark 1.** In adhesive categories, for every finite family $J$ of matches the colimits exist (as iterated pushouts along monomorphisms), the morphism $r_s$ is a monomorphism, and all rules $r_j$ are subrules of the resulting multi-amalgamated rule $r_s$ [6]. In practical applications, e.g., when working with finite graph-like structures, this property is automatically fulfilled.
For formalizing our intended construction, we need a way to express the
difference between objects in the setting of adhesive categories. The concept of
initial pushouts [4] allows for this.

**Definition 4 (Initial pushout).** *Given a morphism* $e: E \to P$, *an initial pushout over* $e$ *is a pushout (0) as in the left square below such that* $b_P$ *is a monomorphism and the pushout (0) factors as a pushout (1) uniquely through every pushout (2) over e where* $b'_P$ *is a monomorphism as in the right diagram below. Given an initial pushout (0) over e, $B_P$ *is called the boundary object and* $C_P$ *the context object with respect to e.*

<figure><img src="image_12.png" /></figure>

In the category of sets, if the morphism $e: E \to P$ is injective, the set $B_P$ is empty and $C_P$ is isomorphic to $P \setminus e(E)$. In the category of graphs, if $e$ is injective, $C_P$ is the graph arising by adding to $P \setminus e(E)$ those nodes from $E$ necessary to complete it to a graph and $B_P$ consists exactly of those *boundary nodes*. Thus, $B_P$ consists of those nodes of $E$ which get mapped to a node with an adjacent edge in $P$ that has no preimage in $E$. Thus, we will often use $P \setminus E$ instead of $C_P$ to denote the context object in an initial pushout over a monomorphism.

# 4 Constraint-Preserving Interaction Schemes

In this section, we develop our construction of constraint-preserving and -guaranteeing interaction schemes. We prove the construction to be well-defined, i.e., it results in a family of multi-rules, and present sufficient conditions for the desired preservation property of the arising interaction schemes.

The central idea of the construction of a constraint-preserving interaction
scheme is to identify each way in which the application of a rule may introduce
a violation of a given positive atomic constraint $c = \forall (P, \exists C)$. These are the
different ways in which the rule can create a new occurrence of $P$. For each
such situation we derive a multi-rule that additionally amends this new $P$ to $C$.
Applying the such arising interaction scheme instead of the original rule preserves
the validity of the constraint (if the multi-rules themselves do not introduce new
violations again). Slightly extending this strategy additionally provides rules
that repair already existing violations of the constraint, i.e., enable to not only
preserve but guarantee consistency.

We first introduce *compatible rule-constraint intersections* to classify the
ways in which a rule $r: L \to R$ may introduce an image of the premise $P$ of
a constraint $\forall (P, \exists C)$. Assuming a transformation $G \Rightarrow_{r,m} H$ to be given, the
co-match is an embedding of $R$ in $H$. If there is an image of $P$ in $H$, it intersects
with that image of $R$ in $H$ (maybe emptily). This intersection restricts to an intersection between the images of $L$ and $P$ in $H$ as well. Thus, we introduce compatible intersections as monomorphisms $\iota : D \hookrightarrow E$ where $E$ is a subobject of $R$ and $P$ and $D$ is a subobject of $L$ and $P$ in a compatible way. The intuition is that $D$ is that part of $P$ already matched by the rule and $E \setminus D$ is the part the rule's application created anew. This suggests that if $\iota$ is an isomorphism, a situation is captured where the rule only matches some part of an image of $P$ without creating a part of it (compare Lemma 2). We only need to consider those intersections that actually stem from applications of rules. Thus, calculating all such intersections gives all conceivable different ways in which an application of the rule might introduce a new subobject (isomorphic to) $P$.

**Definition 5 (Compatible rule-constraint intersection).** Let $\mathcal{C}$ be an adhesive category, $r : L \hookrightarrow R$ a monotonic rule, and $c = \forall (P, \exists C) \text{ a positive atomic constraint in } \mathcal{C}$. A compatible rule-constraint intersection for $r$ and $c$ is a pair of spans of monomorphisms $d : L \xleftarrow{d_L} D \xrightarrow{d_P} P$ and $e : R \xleftarrow{e_R} E \xrightarrow{e_P} P$ with monomorphism $\iota : D \hookrightarrow E$ such that (compare Fig. 10)

1. $d_P = e_P \circ \iota$,

2. the square (1) is a pullback, i.e., $\iota : D \hookrightarrow E$ is a subrule of $r$, and

3. there exists an object $H$ and monomorphisms $n_1 : R \hookrightarrow H$ and $m_2 : P \hookrightarrow H$ such that the arising square (2) is a pullback and a pushout complement $G$ for $n_1 \circ r$ exists (i.e., the rule $r^{-1}$ is applicable at $H$ with match $n_1$).

<figure><img src="image_13.png" /><figcaption>**Fig. 10.** Compatible intersections</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>**Fig. 11.** Construction of the multi-rule $r_{d,e}$</figcaption></figure>

*Example 1.* The diagram in Fig. 12 depicts a compatible rule-constraint intersection for rule *createEntry* and the constraint *PropagationOfEntries*. It is the only compatible intersection for them where $\iota$ is not an isomorphism. Only intersecting the node of type *Entry* from the rule's RHS with the one from the constraint's premise (inducing an empty intersection between the LHS and the premise) leads
to a pair of intersections that satisfy the first two properties of Definition 5 but
not the third one: It is not possible that an application of *createEntry* only creates
the node of type *Entry* of an occurrence of the premise but not its corresponding
incoming edge of type *ownedEntry* as this would imply that the edge existed
without a target node before the application of the rule *createEntry* which is not
allowed in a graph.

<figure><img src="image_15.png" /><figcaption>**Fig. 12.** Compatible rule-constraint intersection for rule *createEntry* and constraint *PropagationOfEntries* (node names indicate the morphisms)</figcaption></figure>

In the example above, the node doc2 is a (in fact the only) boundary element: When deleting *E* from *P*, this node needs to be added to the result again for it to become a graph (so that the edge of type *refDoc* is not dangling). This signifies that this node must have existed before application of the rule and is one of the places (here even *the place*) at which *E* and *P* \ *E* are glued to receive a complete copy of *P*. Hence, this node needs to be matched by the rule application to create *P* and, thus, is already part of *D*, the intersection of *L* and *P*. The next lemma states that this generalizes, i.e., the boundary object *B*<sub>*P*</sub> is always a subobject of *D* and the existence of this inclusion morphism is vital for our construction.

**Lemma 1 (Covering of boundary elements).** Let $\mathcal{C}$ be an adhesive category with initial pushouts, $r : L \hookrightarrow R$ a rule, $c = \forall (P, \exists p : P \hookrightarrow C)$ a constraint in $\mathcal{C}$, and $(d : L \hookleftarrow D \hookrightarrow P, e : R \hookleftarrow E \hookrightarrow P)$ with monomorphism $\iota : D \hookrightarrow E$ a compatible rule-constraint intersection. Let $B_P$ be the boundary object of the initial pushout over $e_P : E \hookrightarrow P$. Then there exists a monomorphism $x : B_P \hookrightarrow D$ such that $\iota \circ x = b_P$. In particular, $B_P$ is a pullback object for the monomorphisms $\iota : D \hookrightarrow E$ and $b_P : B_P \hookrightarrow E$ (compare Fig. 10).

Given a compatible rule-constraint intersection $(d, e)$, we use it to compute a multi-rule $r_{d,e}$. Its RHS is just the join of $R$ and $C$ along $E$, thus completing a newly created $P$ to $C$. The multi-rule $r_{d,e}$ should match exactly in those cases where $r$ creates a new $P$ by adding $E \setminus D$ to some already existing structure. Thus, $P$ has to exist except for the part $E \setminus D$ before rule application and the multi-rule needs to match that structure. This is achieved by joining $L$ with the join of $P \setminus E$ and $D$ along the boundary object $B_P$.

**Construction 1 (Constraint-guaranteeing and constraint-preserving interaction scheme).** Let $\mathcal{C}$ be an adhesive category with initial pushouts,
$r: L \leftrightarrow R$ a monotonic rule, and $c = \forall (P, \exists p : P \to C)$ a positive atomic constraint in $C$. For each (up to isomorphism) compatible rule-constraint intersection $(d : L \underset{d_L}{\leftrightarrow} D \underset{d_P}{\leftrightarrow} P, e : R \underset{e_R}{\leftrightarrow} E \underset{e_P}{\leftrightarrow} P)$ with monomorphism $\iota : D \to E$ for $r$ and $c$, compute the multi-rule $r_{d,e} : L_{d,e} \leftrightarrow R_{d,e}$ in the following way (compare Fig. 11):

1. Compute the LHS $L_{d,e}$ of $r_{d,e}$ as pushout of the morphisms $d_L \circ x : B_P \to L$ and $B_P \to P \setminus E$.

2. Compute the RHS $R_{d,e}$ of $r_{d,e}$ as pushout of the morphisms $e_R : E \to R$ and $p \circ e_P : E \to C$.

3. The morphism $r_{d,e} : L_{d,e} \to R_{d,e}$ is induced by the universal property of the pushout computing $L_{d,e}$.

The constraint-guaranteeing interaction scheme for $r$ with respect to $c$ consists of the arising multi-rules and is denoted with $ias_{r,c}$. Its restriction $ias_{r,c}^p$ consists of those multi-rules stemming from pairs of intersections $(d,e)$ where $\iota : D \to E$ is not an isomorphism and is called constraint-preserving interaction scheme.

**Example 2.** Given the rule *createEntry* and the constraint *PropagationOfEntries*, the constraint-preserving interaction scheme consists only of the kernel morphism that embeds *createEntry* into the multi-rule *createEntry-multi* as depicted in Fig. 5. That is because the only possible choice for a compatible rule-constraint intersection that is not an isomorphism is the one presented in Example 1.

The constraint-guaranteeing interaction scheme additionally contains the multi-rules depicted in Fig. 13. The intersections from which they are arising are given by the two isomorphisms from the empty graph to itself and from one node of type *Doc* to itself, respectively. The node of type *Doc* then might by identified with each of the two nodes of type *Doc* occurring in the constraint.

<figure><img src="image_16.png" /><figcaption>**Fig. 13.** Additional multi-rules contained in the constraint-guaranteeing interaction scheme of rule *createEntry* and constraint *PropagationOfEntries*</figcaption></figure>

**Remark 2.** We introduced interaction schemes, as usual, as *finite sets* in *Definition 3*. For the construction of the amalgamated rule (Definition 3 and Remark 1) it is important that the set $J$ is finite – otherwise the colimits might not exist. The most natural setting to guarantee that both the interaction schemes arising
by the above construction and the number of matches in their maximal matchings are finite is that of finitary categories, i.e., categories where every object has only finitely many subobjects. Moreover, in finitary adhesive categories initial pushouts always exist [5, Fact 3.12] – thus they do not need to be required as additional precondition. But since, for the above construction, the number of compatible rule-constraint intersections is not relevant and the number of matches in a maximal matching might be finite even if the considered interaction scheme is not, we did not restrict ourselves to finitary categories.

rule exploits the van Kampen property of the cube in Fig. 11; in this way the right front face is a pullback.

**Theorem 1 (Well-definedness of construction).** Let $\mathcal{C}$ be an adhesive category with initial pushouts, $r : L \hookrightarrow R$ a monotonic rule, and $c = \forall (P, \exists p : P \hookrightarrow C)$ a positive atomic constraint in $\mathcal{C}$. Then for every compatible rule-constraint intersection $(d, e)$ the rule $r_{d,e} : L_{d,e} \hookrightarrow R_{d,e}$ as introduced in Construction 1 is a multi-rule of $r$ and the morphism $r_{d,e}$ is a monomorphism.

The next lemma states that compatible rule-constraint intersections are capable of distinguishing if an application of a rule $r$ first enabled a matching of $P$ in $H$ or if this match already restricts to a match in $G$ where $G \Rightarrow_r H$.

**Lemma 2 (Classification of compatible rule-constraint intersections).**

Let $\mathcal{C}$ be an adhesive category with initial pushouts, $r : L \hookrightarrow R$ a monotonic rule, $c = \forall (P, \exists p : P \hookrightarrow C)$ a positive atomic constraint, and $(d : L \stackrel{d_L}{\hookleftarrow} D \stackrel{d_P}{\hookrightarrow} P, e : R \stackrel{e_R}{\hookleftarrow} E \stackrel{e_P}{\hookrightarrow} P)$ with morphism $\iota : D \hookrightarrow E$ a compatible rule-constraint intersection for the rule $r$ and the premise $P$ of the constraint $c$. Let $H$ be an object with monomorphisms $n_1 : R \hookrightarrow H$ and $m_2 : P \hookrightarrow H$ such that the induced square is a pullback and a pushout complement $G$ for $n_1 \circ r$ exists. Then $P$ already embeds into $G$ in a way compatible to its embedding in $H$ if and only if $\iota : D \hookrightarrow E$ is an isomorphism.

Intuitively, applying the original rule $r$ and the complement rules of the constructed interactions scheme afterwards, these complement rules supplement each currently existing image of the premise $P$ of the constraint with an image of its conclusion $C$. But it may happen that the application of such complement rules introduces new occurrences of $P$ which, by nature of our construction, are not supplemented. Consequently, it may happen that after applying the interaction scheme the constraint is violated, nonetheless. The next definition serves to be able to exclude situations like that rigorously and assumes familiarity with the concept of parallel independence [4]. The subsequent theorem states that this condition of independence is a sufficient (not necessary) condition for the constructed interaction schemes to preserve (guarantee) consistency with respect to a constraint. Its proof uses this independence to show that occurrences of $P$ must stem from application of $r$ or have already existed before. Then one needs to check that each such situation is covered by a multi-rule which is done by showing the arising intersections to be compatible (see Definition 5).
**Definition 6 (Complementable).** Given a monotonic rule $r: L \hookrightarrow R$ and a positive atomic constraint $c = \forall (P, \exists C)$, $r$ is called (strongly) complementable with respect to $c$ if for every multi-rule $r_{d,e}: L_{d,e} \hookrightarrow R_{d,e}$ from the interaction scheme $ias_{r,c}^p$ ($ias_{r,c}$) the inverse of its complement rule and the constant rule $P \hookrightarrow P$ are parallel independent.

**Theorem 2 (Guarantee and preservation).** Let an adhesive category $\mathcal{C}$ with initial pushouts be given. Let $r: L \hookrightarrow R$ be a monotonic rule, $c = \forall (P, \exists p : P \hookrightarrow \mathcal{C})$ a positive atomic constraint, and $ias_{r,c}$ and $ias_{r,c}^p$ the constraint-guaranteeing and constraint-preserving interaction schemes from Construction 1, respectively. Let $m_1$ be a match for $r$ at an arbitrary object $G$ with maximal matchings $J$ and $J^p$ for $ias_{r,c}$ and $ias_{r,c}^p$ extending $m_1$.

1. If $r$ is strongly complementable with respect to $c$ and $J$ is finite, then the object $H$ arising by application of $ias_{r,c}$ with that matching satisfies the constraint $c$.

2. If $r$ is complementable with respect to $c$ and $J^p$ is finite then the object $H$ arising by application of $ias_{r,c}$ with that matching satisfies the constraint $c$.

# 5 Prospects and Future Work

This paper focuses on presenting the general idea behind the construction of constraint-preserving interaction schemes and proving their fundamental property. However, there are a lot of possible refinements and interesting future work:

In adhesive categories with strict initial object $\emptyset$, a constraint of the form $\exists C$, which requires $C$ to be a subobject of $G$ to be valid for an object $G$, is semantically equivalent to $\forall (\emptyset, \exists \emptyset \hookrightarrow C)$, i.e., preservation or guarantee of those constraints is dealt with in our framework as well.

The general idea presented in this paper may be used for deleting rules $r = (L \hookrightarrow K \hookrightarrow R)$ as long as it is not possible that an application of that rule deletes an occurrence $C$ of the relevant constraint $\forall (P, \exists C)$, e.g., always when $L \setminus K$ and $C$ intersect emptily. The construction stays the same, in principle, with $K$ playing the role of $L$. The difference is that every arising multi-rule gets equipped with left-hand side $L_{d,e}$ arising as pushout of $K \hookrightarrow L$ and $K \hookrightarrow K_{d,e}$.

The precondition of complementability that comes with Theorem 2 is a severe restriction. There are examples, where this precondition is not met, but where recursively repeating our construction for the computed multi-rules again terminates (with no new multi-rules arising anymore) and where these multi-rules of multi-rules can be equivalently expressed as simple multi-rules of the original rule and the constraint is preserved by that extended interaction scheme. We give an example for this, namely a constraint requiring transitive closure over edges of a certain type, in the extended version of this paper [11]. Investigating this possibility in more detail is future work.

We plan to further integrate application conditions into our approach. Another topic for future research is to support preservation or guarantee of more than one constraint simultaneously. It would be especially interesting to combine support
for positive atomic constraints and negative ones of the form $\neg\exists C$, forbidding $C$ to be an subobject of $G$ to be valid for $G$. Our vision is to characterize those combinations of rules and constraints such that it is possible to preserve consistency with the whole set of constraints by incorporating the negative ones as application conditions into the rules and then constructing the preserving interaction schemes to support the positive atomic ones.

# 6 Related Work

As already discussed in *Sect. 1* and *2*, our work can be seen as a continuation of [13] and a supplement to [7]. To the best of our knowledge, we are the first to suggest an automatable construction to alter a rule into an interaction scheme to preserve consistency with respect to a given constraint.

We are aware of two works, both with tool support, allowing for automatic construction of interaction schemes in the context of EMF model transformation, but none of them explicitly aims at preservation of constraints. In [1], Alshanqiti et al. derive visual contracts from Java programs. They monitor the execution of programs and generate transformation rules describing the behavior of the program. The process supports the generation of interaction schemes. In contrast to our work aiming at preservation of constraints, their derived rules provide an abstract and visual representation of observed behavior.

Kehrer et al. [9] allow a user to specify examples of how a transformation should (or should not) act and from that infer a rule subsuming the provided examples. Their tool is also able to derive interaction schemes. As above, the aim is not to preserve correctness of an explicitly given constraint, and a generated interaction scheme may or may not happen to do so (depending on the quality of the input of the user) or serve a completely different purpose.

There are two works, [15,16] and [8], that derive repair programs from (graph) constraints. In both works, given a set of constraints, a set of rules and some control results in an instance satisfying those constraints. In neither case interaction schemes are derived, but by passing of parameters or marking and applying rules as often as possible, the same effects are achieved. The second work is done in the context of (labeled) graphs and supports quite a large class of graph constraints, though support for sets of constraints is limited. The first one is done in the context of EMF models and repairs violations of multiplicities while respecting the in-built constraints of EMF. Moreover, it is implemented [16].

In [2], Becker et al. propose a method to design consistency-preserving rule-based refactorings. Given such a refactoring and a constraint, an invariant checker provides the user with minimal counterexamples for situations in which the refactoring does not preserve consistency with respect to the constraint. The user may use this information to redesign the refactoring and iterate over this process. The class of supported constraints is slightly larger than ours (supporting also negative constraint). Refactorings are specified via graph transformation rules and though there is no explicit support for interaction schemes, it is possible
to use marking and iterate the application of rules as often as possible, which
can have the same effect. If a constraint-preserving specification of a refactoring
is achieved, of course, depends on the user.

In [10], Kehrer et al. automatically derive edit rules from meta-models. Start-
ing with atomic operations, they revise rules such that elementary consistency
constraints, necessary to be met for a model to be opened in a typical editor,
are preserved on application of those roles. When viewing lower bounds of multi-
plicities of containment edges as positive atomic constraints and applying our
construction to these constraints and their elementary rules for node creation, we
receive exactly the rules they are using, too. In this case, however, the resulting
rules actually not are multi-rules since the LHSs of the resulting multi-rules are
the LHSs of the original rules again.

7 Conclusion

In the setting of adhesive categories, given a positive atomic constraint and
a monotonic rule, we presented a construction of a constraint-preserving (or
-guaranteeing) interaction scheme. We showed that our construction is well-
defined and gave (sufficient) conditions under which the constraint is preserved
(or guaranteed) when applying the resulting interaction schemes. With this
approach, we are aiming at being able to replace the computation of constraint-
preserving (or -guaranteeing) application conditions for rules in a situation where
this has the often undesired effect of severely restricting the applicability of
the rule. With our approach we are already able to automate the construction
of multi-rules that had to be developed by hand before in [13]. We pointed at
promising directions of research to be able to generalize our construction, to
overcome the precondition of complementability that was necessary for our main
theorem to hold, and to increase the effectiveness of our method in practice.

**Acknowledgments** This work was partially funded by the German Research Foundation (DFG), projects "Triple Graph Grammars (TGG) 2.0" and "Generating Development Environments for Modeling Languages". We thank Erhan Leblebici for many helpful remarks.

References

1. Alshanqiti, A., Heckel, R., Kehrer, T.: Inferring visual contracts from Java programs. Automated Software Engineering **25**(4), 745–784 (2018)

2. Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: Iterative Development of Consistency-Preserving Rule-Based Refactorings. In: Cabot, J., Visser, E. (eds.) Theory and Practice of Model Transformations. pp. 123–137. Springer, Berlin (2011)

3. Biermann, E., Ermel, C., Taentzer, G.: Formal foundation of consistent EMF model transformations by algebraic graph transformation. Software & Systems Modeling **11**(2), 227–250 (2012)
4. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science, Springer (2006)

5. Gabriel, K., Braatz, B., Ehrig, H., Golas, U.: Finitary M-adhesive categories. Mathematical Structures in Computer Science 24(4), 240403 (2014)

6. Golas, U., Habel, A., Ehrig, H.: Multi-amalgamation of rules with application conditions in M-adhesive categories. Math. Struct. in Comp. Science 24 (2014)

7. Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. in Comp. Science 19, 245–296 (2009)

8. Habel, A., Sandmann, C.: Graph Repair by Graph Programs. In: Mazzara, M., Ober, I., Salaün, G. (eds.) Software Technologies: Applications and Foundations. pp. 431–446. Springer International Publishing, Cham (2018)

9. Kehrer, T., Alshanqiti, A., Heckel, R.: Automatic Inference of Rule-Based Specifications of Complex In-place Model Transformations. In: Guerra, E., van den Brand, M. (eds.) Theory and Practice of Model Transformation. pp. 92–107. Springer, Cham (2017)

10. Kehrer, T., Taentzer, G., Rindt, M., Kelter, U.: Automatically deriving the specification of model editing operations from meta-models. In: Van Gorp, P., Engels, G. (eds.) Theory and Practice of Model Transformations. pp. 173–188. Springer, Cham (2016)

11. Kosiol, J., Fritsche, L., Nassar, N., Schürr, A., Taentzer, G.: Constructing Constraint-Preserving Interaction Schemes in Adhesive Categories: Extended Version. Tech. rep., Philipps-Universität Marburg (2019), https://www.uni-marburg.de/fb12/arbeitsgruppen/swt/forschung/publikationen/2019/KFNST19-TR.pdf

12. Lack, S., Sobociński, P.: Adhesive and quasiadhesive categories. Theoretical Informatics and Applications 39(3), 511–545 (2005)

13. Leblebici, E., Anjorin, A., Schürr, A., Taentzer, G.: Multi-amalgamated triple graph grammars: Formal foundation and application to visual language translation. Journal of Visual Languages & Computing 42, 99–121 (2017)

14. Nassar, N., Kosiol, J., Arendt, T., Taentzer, G.: OCL2AC. Automatic Translation of OCL Constraints to Graph Constraints and Application Conditions for Transformation Rules. In: Lambers, L., Weber, J. (eds.) Graph Transformation. pp. 171–177. Springer International Publishing, Cham (2018)

15. Nassar, N., Kosiol, J., Radke, H.: Rule-based Repair of EMF Models: Formalization and Correctness Proof. In: Corradini, A. (ed.) Graph Computation Models (GCM 2017), Electronic Pre-Proceedings (2017), pages.di.unipi.it/corradini/Workshops/GCM2017/papers/Nassar-Kosiol-Radke-GCM2017.pdf

16. Nassar, N., Radke, H., Arendt, T.: Rule-based repair of emf models: An automated interactive approach. In: Guerra, E., van den Brand, M. (eds.) Theory and Practice of Model Transformation. pp. 171–181. Springer, Cham (2017)

17. OMG: Object Constraint Language, http://www.omg.org/spec/OCL/

18. Radke, H., Arendt, T., Becker, J.S., Habel, A., Taentzer, G.: Translating essential OCL invariants to nested graph constraints for generating instances of meta-models. Science of Computer Programming 152, 38–62 (2018)

19. Rensink, A.: Representing First-Order Logic Using Graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) Graph Transformations. pp. 319–335. Springer, Berlin (2004)

20. Schürr, A.: Specification of Graph Translators with Triple Graph Grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) Graph-Theoretic Concepts in Computer Science. pp. 151–163. Springer (1995)