Modular Termination of Graph Transformation

Abstract

We establish a machine-checkable condition which ensures that the union of two terminating hypergraph transformation systems is terminating. The condition is based on so-called sequential critical pairs which represent consecutive rule applications that are not independent. In contrast to a corresponding modularity result for term rewriting, no restrictions on the form of rules are required. Our result applies to both systems with injective rules and systems with rules that merge nodes or edges.

1 Introduction

In the area of graph transformation, the problem of proving that a system will terminate (admit only a finite number of rule applications) on arbitrary host graphs has received surprisingly little attention. This is in contrast to the central role of termination research in the area of term rewriting [1, 2].

Work on proving termination of general graph transformation systems by various methods includes [3,4,5, 16]. There are also some papers on termination in the specialised settings of term graph rewriting [14, 15, 17] and cycle rewriting [21, 23].

In this paper, we are interested in the problem of finding conditions that guarantee that the combination of terminating (hyper-)graph transformation systems yields again a terminating system. The corresponding problem for term rewriting systems received considerable attention after Toyama showed that even the combination of systems with disjoint function symbols need not preserve termination [22]. Interestingly, the latter phenomenon vanishes into thin air for acyclic term graph rewriting [14, 15] because rewrite steps create shared subgraphs instead of copying subterms.

We prove in this paper that the union of two general hypergraph transformation systems preserves termination if there are no critical overlaps between the right-hand sides of one system and the left-hand sides of the other system. This idea is inspired by a result of Dershowitz [7] which shows that the corresponding property for term rewriting systems holds if one of the systems is left-linear and the other system is right-linear. In the case of graph transformation, it turns out that no restrictions on the form of rules are needed.

The rest of this paper is organized as follows. In Sect. 2, we review the basics of hypergraph transformation. In particular, we recall the concept of sequential independence which is crucial for our main result. Sequential critical pairs are introduced in Sect. 3, in analogy to standard critical pairs for graph transformation. Our main result is proved in Sect. 4 where we also give examples to demonstrate the application of the modularity criterion. We conclude in Sect. 5.

2 Hypergraph Transformation

In this section, we recall some definitions and results of the double-pushout approach to graph transformation which can be found, for example, in [11]. For generality, we use here the setting of hypergraphs.

2.1 Hypergraphs

Our hypergraphs are directed and labelled. We use a type system where the label of a hyperedge can restrict the number of incident nodes and their labels. A signature $\varSigma = \langle \varSigma _{\mathrm {V}},\varSigma _{\mathrm {E}},\mathrm {Type}\rangle$ consists of a set $\varSigma _{\mathrm {V}}$ of node labels, a set $\varSigma _{\mathrm {E}}$ of hyperedge labels and a function $\mathrm {Type}$ assigning to each $l \in \varSigma _{\mathrm {E}}$ a set of strings $\mathrm {Type}(l) \subseteq \varSigma _{\mathrm {V}}^*$. This kind of typing allows to “overload” hyperedge labels by specifying different admissible attachment sequences. Typing regimes covered by this approach include the case of a singleton set $\mathrm {Type}(l)$ for each label l (as in [6]) and the case of “untyped” hypergraphs given by $\mathrm {Type}(l) = \varSigma _{\mathrm {V}}^*$ for each l (as in [10]). Unless stated otherwise, we denote by $\varSigma$ an arbitrary but fixed signature over which all hypergraphs are labelled.

A hypergraph over $\varSigma$ is a system $G = \langle \mathrm {V}_G, \mathrm {E}_G, \mathrm {mark}_G, \mathrm {lab}_G, \mathrm {att}_G\rangle$ consisting of two finite sets $\mathrm {V}_G$ and $\mathrm {E}_G$ of nodes (or vertices) and hyperedges, two labelling functions $\mathrm {mark}_G:\mathrm {V}_G \rightarrow \varSigma _{\mathrm {V}}$ and $\mathrm {lab}_G:\mathrm {E}_G \rightarrow \varSigma _{\mathrm {E}}$, and an attachment function $\mathrm {att}_G:\mathrm {E}_G \rightarrow \mathrm {V}_G^*$ such that $\mathrm {mark}_G^*(\mathrm {att}_G(e)) \in \mathrm {Type}(\mathrm {lab}_G(e))$ for each hyperedge e. (The extension $f^*:A^* \rightarrow B^*$ of a function $f:A \rightarrow B$ maps the empty string to itself and $a_1 \dots a_n$ to $f(a_1) \dots f(a_n)$.)

In pictures, nodes and hyperedges are drawn as circles and boxes, respectively, with labels inside. Lines represent the attachment of hyperedges to nodes, where numbers specify the left-to-right order in the attachment string. For example, Fig. 1 shows a hypergraph with four nodes (all labelled with $\bullet$) and three hyperedges (labelled with B and S).

Fig. 1.

A hypergraph

A hypergraph G is a graph if each hyperedge e is an ordinary edge, that is, if $\mathrm {att}_G(e)$ has length two. Ordinary edges may be drawn as arrows with labels written next to them.

Given hypergraphs G and H, a hypergraph morphism (or morphism for short) $g:G \rightarrow H$ consists of two functions $g_{\mathrm {V}}:\mathrm {V}_G \rightarrow \mathrm {V}_H$ and $g_{\mathrm {E}}:\mathrm {E}_G \rightarrow \mathrm {E}_H$ that preserve labels and attachment to nodes, that is, $\mathrm {mark}_H \circ g_{\mathrm {V}} = \mathrm {mark}_G$, $\mathrm {lab}_H \circ g_{\mathrm {E}} = \mathrm {lab}_G$ and $\mathrm {att}_H \circ g_{\mathrm {E}} = g_{\mathrm {V}}^* \circ \mathrm {att}_G$. A morphism $incl:G \rightarrow H$ is an inclusion if $incl_{\mathrm {V}}(v) = v$ and $incl_{\mathrm {E}}(e) = e$ for all $v \in \mathrm {V}_G$ and $e \in \mathrm {E}_G$. In this case G is a subhypergraph of H which is denoted by $G \subseteq H$. Morphism g is injective (surjective) if $g_V$ and $g_E$ are injective (surjective). If g is both injective and surjective, then it is an isomorphism. In this case G and H are isomorphic, which is denoted by $G \cong H$.

The composition of two morphisms $g:G \rightarrow H$ and $h:H \rightarrow M$ is the morphism $h \circ g:G \rightarrow M$ consisting of the composed functions $h_{\mathrm {V}} \circ g_{\mathrm {V}}$ and $h_{\mathrm {E}} \circ g_{\mathrm {E}}$. The composition is also written as $G \rightarrow H \rightarrow M$ if g and h are clear from the context.

2.2 Rules and Derivations

A rule $r:\langle L \leftarrow K \rightarrow R\rangle$ consists of two hypergraph morphisms with a common domain, where $K \rightarrow L$ is an inclusion. The hypergraphs L and R are the left- and right-hand side of r, and K is the interface. The rule is injective if the morphism $K \rightarrow R$ is injective.

Let G and H be hypergraphs, $r:\langle L \leftarrow K \rightarrow R\rangle$ a rule and $g:L \rightarrow G$ an injective morphism. Then G directly derives H by r and g, denoted by $G \Rightarrow _{r,g} H$, if there exist two pushouts as in Fig. 2. Given a set of rules $\mathcal {R}$, we write $G \Rightarrow _{\mathcal {R}} H$ to express that there exist $r \in \mathcal {R}$ and a morphism g such that $G \Rightarrow _{r,g} H$.

Fig. 2.

A double-pushout

We refer to [20] for the definition and construction of hypergraph pushouts. Intuitively, the left pushout corresponds to the construction of D from G by removing the items in $L - K$, and the right pushout to the construction of H from D by merging items according to $K \rightarrow R$ and adding the items in R that are not in the image of K.

A double-pushout as in Fig. 2 is called a direct derivation from G to H and may be denoted by $G \Rightarrow _{r,g} H$ or just by $G \Rightarrow _r H$ or $G \Rightarrow H$. A derivation from G to H is a sequence of direct derivations $G_0 \Rightarrow \dots \Rightarrow G_n$, $n \ge 0$, such that $G \cong G_0$ and $G_n \cong H$. We write $G \Rightarrow ^*H$ for such a derivation or $G \Rightarrow ^*_{\mathcal {R}} H$ if all rules used in the derivation are from $\mathcal {R}$.

Given a rule $r:\langle L \leftarrow K \rightarrow R\rangle$, an injective morphism $g:L \rightarrow G$ satisfies the dangling condition if no hyperedge in $\mathrm {E}_G - g_{\mathrm {E}}(\mathrm {E}_L)$ is incident to a node in $g_{\mathrm {V}}(\mathrm {V}_L - \mathrm {V}_K)$. It can be shown that, given r and f, a direct derivation as in Fig. 2 exists if and only if g satisfies the dangling condition [11].

Definition 1

(Hypergraph transformation system). A hypergraph transformation system $\langle \varSigma ,\mathcal {R}\rangle$ consists of a signature $\varSigma$ and a finite set $\mathcal {R}$ of rules over $\varSigma$. The system is injective if all rules in $\mathcal {R}$ are injective. It is a graph transformation system if for each label l in $\varSigma _{\mathrm {E}}$, all strings in $\mathrm {Type}(l)$ are of length two.

Note that since graph transformation systems are special hypergraph transformation systems, results for the latter usually apply to the former, too.

Example 1

Figure 3 shows hypergraph transformation rules for reducing control-flow graphs [20]. The associated signature contains a single node label $\bullet$ and two hyperedge labels which are graphically represented by hyperedges formed as squares and rhombs. Instead of using numbers to represent the attachment function, we use an arrow to point to the second attachment node of a square and define the order among the links of a rhomb to be “top-left-right”. The rules are shown in a shorthand notation where only the left- and right-hand sides are depicted, the interface and the morphisms are implicitly given by the node names x, y, z.    $\square$

Fig. 3.

Hypergraph transformation system for flow-graph reduction

2.3 Sequential Independence

Given injective rules $r_1$ and $r_2$, consecutive direct derivations $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$ do not interfere with each other if the intersection of the right-hand side of $r_1$ with the left-hand side of $r_2$ in H consists of common interface items. In the presence of non-injective rules, however, independence needs to be defined in terms of the existence of certain morphisms. We give the general definition first and then consider a simpler condition for the case of injective rules. For $i=1,2$, let $r_i$ denote a rule $\langle L_i \leftarrow K_i \rightarrow R_i\rangle$.

Definition 2

(Sequential independence). Direct derivations $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$ as in Fig. 4 are sequentially independent if there are morphisms $R_1 \rightarrow D_2$ and $L_2 \rightarrow D_1$ such that the following holds.

• Commutativity: $R_1 \rightarrow D_2 \rightarrow H = R_1 \rightarrow H$ and $L_2 \rightarrow D_1 \rightarrow H = L_2 \rightarrow H$.

• Injectivity: $R_1\rightarrow D_2 \rightarrow M$ is injective.

Fig. 4.

Sequentially independent direct derivations

The injectivity requirement for $R_1\rightarrow D_2 \rightarrow M$ is needed in case $r_2$ is non-injective. See [11] for an example that the steps $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$ may not be interchangeable without this condition.

If $r_1$ and $r_2$ are injective, the direct derivations of Fig. 4 are independent if and only if the intersection of $R_1$ and $L_2$ in H coincides with the intersection of $K_1$ and $K_2$. Moreover, the injectivity condition of Definition 2 is automatically satisfied.

Lemma 1

(Independence for injective rules). Let rules $r_1$ and $r_2$ in Fig. 4 be injective. Then the following are equivalent:

• (1) $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$ are sequentially independent.

• (2) There are morphisms $R_1 \rightarrow D_2$ and $L_2 \rightarrow D_1$ such that $R_1 \rightarrow D_2 \rightarrow H = R_1 \rightarrow H$ and $L_2 \rightarrow D_1 \rightarrow H = L_2 \rightarrow H$.

• (3) $h(R_1) \cap g(L_2) = h(b(K_1)) \cap g(K_2)$ where $h:R_1 \rightarrow H$, $g:L_2 \rightarrow H$ and $b:K_1 \rightarrow R_1$. (Note that $K_2 \rightarrow L_2$ is an inclusion.)

Proof

The equivalence of (1) and (2) is an easy consequence of the fact that with injective rules, all morphisms in Fig. 4 are injective. The equivalence of (2) and (3) is shown in [9, 19].    $\square$

The following theorem was originally proved in [8], in the setting of graph transformation with arbitrary, possibly non-injective matching morphisms. This proof was adapted in [19] to the setting of hypergraph transformation with injective matching.

Theorem 1

([11, 19]). Given sequentially independent direct derivations $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$, there exist direct derivations of the form $G \Rightarrow _{r_2} H' \Rightarrow _{r_1} M$.

For instance, Fig. 5 shows applications of the rules seq and dec2 from Example 1. The steps are independent because the occurrences of the right-hand side of seq and the left-hand side dec2 share only nodes y and z, which are interface nodes in both rules. Hence the steps can be interchanged, leading to the same result.

Fig. 5.

Sequentially independent rule applications

3 Sequential Critical Pairs

Standard critical pairs represent conflicts between rule applications to the same graph and are used to analyse graph transformation systems for local confluence [20]. In the context of verifying termination, we adapt this concept to represent conflicts between consecutive direct derivations.

Fig. 6.

A sequential critical pair

Sequential critical pairs are minimal derivations of length two whose steps are not independent. Due to the minimality, the set of critical pairs induced by two hypergraph transformation rules is finite and can be constructed. We will see that if this set is empty, then any pair of direct derivations with these rules is sequentially independent. In the proof of the main result, this will enable us to re-order the rule applications of infinite derivations.

Definition 3

(Sequential critical pair). Let $r_i:\langle L_i \leftarrow K_i \rightarrow R_i\rangle$ be rules, for $i=1,2$. A pair of direct derivations $S \Rightarrow _{r_1} T \Rightarrow _{r_2} U$ as in Fig. 6 is a sequential critical pair if the following holds.

• Minimality: $T = h_1(R_1) \cup g_2(L_2)$.

• Conflict: The steps are not sequentially independent.

Sequential critical pairs $S \Rightarrow _{r_1,g_1} T \Rightarrow _{r_2,g_2} U$ and $S' \Rightarrow _{r_1,g_1'} T' \Rightarrow _{r_2,g_2'} U'$ are isomorphic if there are isomorphisms $i_1:S \rightarrow S'$ and $i_2:T \rightarrow T'$ such that $g_1' = i_1 \circ g_1$ and $g_2' = i_2 \circ g_2$. (This implies that U and $U'$ are isomorphic, too.) From now on we equate isomorphic critical pairs. With the minimality condition of Definition 3 it follows that every hypergraph transformation system has only finitely many critical pairs.

Example 2

Figure 7 shows two sequential critical pairs of the rules of Fig. 3.

Fig. 7.

Two sequential critical pairs of the system of Fig. 3

Lemma 2

For every pair of direct derivations $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$ that are not sequentially independent, there exists a critical pair of the form $S \Rightarrow _{r_1} T \Rightarrow _{r_2} U$.

Proof Sketch

The steps $G \Rightarrow _{r_1} H \Rightarrow _{r_2} M$ can be restricted to a critical pair by removing all nodes and edges that are not used by $r_1$ or $r_2$. That is, S is the subhypergraph of G consisting of all items in the occurrence of the left-hand side of $r_1$ and all items that are preserved by $G \Rightarrow _{r_1} H$ and are in the occurrence of the left-hand side of $r_2$. See [19] for the precise construction. It is not difficult to check that the restricted steps are minimal and in conflict.   $\square$

4 Modular Termination

A hypergraph transformation system $\langle \varSigma ,\mathcal {R}\rangle$ is terminating if there exists no infinite derivation $G_0 \Rightarrow _{\mathcal {R}} G_1 \Rightarrow _{\mathcal {R}} G_2\Rightarrow _{\mathcal {R}} \dots$ The problem to decide whether a system $\langle \varSigma ,\mathcal {R}\rangle$ is terminating is undecidable in general, even for graph transformation systems with injective rules [18].

Theorem 2

(Modular termination). Let $\langle \varSigma ,\mathcal {R}\rangle$ and $\langle \varSigma ,\mathcal {S}\rangle$ be terminating hypergraph transformation systems. If there are no sequential critical pairs of shape $S \Rightarrow _{\mathcal {R}} T \Rightarrow _{\mathcal {S}} U$, then the combined system $\langle \varSigma ,\mathcal {R}\cup \mathcal {S}\rangle$ is terminating.

Note the symmetry in the statement of Theorem 2: it is sufficient that there are no critical pairs of shape $S \Rightarrow _{\mathcal {R}} T \Rightarrow _{\mathcal {S}} U$ or no critical pairs of shape $S \Rightarrow _{\mathcal {S}} T \Rightarrow _{\mathcal {R}} U$.

Proof of Theorem 2. Let $\langle \varSigma ,\,\mathcal {R}\rangle$ and $\langle \varSigma ,\,\mathcal {S}\rangle$ be terminating hypergraph transformation systems such that there are no critical pairs of shape $S \Rightarrow _{\mathcal {R}} T \Rightarrow _{\mathcal {S}} U$. We proceed by contradiction. Suppose there exists an infinite derivation

$$\begin{aligned} G_1 \mathop {\Rightarrow }\limits _{\mathcal {R}\cup \mathcal {S}} G_2 \mathop {\Rightarrow }\limits _{\mathcal {R}\cup \mathcal {S}} G_3 \mathop {\Rightarrow }\limits _{\mathcal {R}\cup \mathcal {S}} \dots \end{aligned}$$

Because $\Rightarrow _{\mathcal {R}}$ and $\Rightarrow _{\mathcal {S}}$ are terminating, the derivation must contain infinitely many steps of both kinds. By Lemma 2, any two steps $G_k \Rightarrow _{\mathcal {R}} G_{k+1} \Rightarrow _{\mathcal {S}} G_{k+2}$ in the sequence are sequentially independent because there are no critical pairs of shape $S \Rightarrow _{\mathcal {R}} T \Rightarrow _{\mathcal {S}} U$. By Theorem 1, the steps can be swapped such that $G_k \Rightarrow _{\mathcal {S}} G'_{k+1} \Rightarrow _{\mathcal {R}} G_{k+2}$. Thus all $\Rightarrow _{\mathcal {S}}$-steps can be pushed back to the beginning of the derivation, resulting in an infinite sequence of $\Rightarrow _{\mathcal {S}}$-steps. This contradicts the fact that $\langle \varSigma ,\,\mathcal {S}\rangle$ is terminating.    $\square$

Figure 8 illustrates the infinite swapping process used to prove Theorem 2. Any infinite derivation with $\mathcal {R}\cup \mathcal {S}$ must contain infinitely many $\mathcal {S}$-steps and hence pushing them to the beginning ad infinitum will build up an infinite derivation of $\mathcal {S}$-steps.

Fig. 8.

Infinite swapping process to create an infinite $\mathcal {S}$-derivation

We now present a sequence of examples which demonstrate the application of Theorem 2.

Example 3

Consider the following graph transformation system from [16]:

It is not obvious that this system is terminating because $r_1$ reduces the number of b-labels in a graph while $r_2$ increases this number. Similarly, $r_2$ reduces the number of c-labels while $r_1$ increases this number.

We can prove that this system is terminating by showing termination of $r_1$ and $r_2$ separately and then applying Theorem 2. Each rule individually is terminating because $r_1$ reduces the number of b’s and $r_2$ reduces the number of c’s. Moreover, there are no critical pairs of shape $S \Rightarrow _{r_2} T \Rightarrow _{r_1} U$. This is because the middle node in the right-hand side of $r_2$ is created by the rule and hence cannot have an incoming a-edge. Thus, by Theorem 2, the combined system is terminating.

Note that the system does have a critical pair of shape $S \Rightarrow _{r_1} T \Rightarrow _{r_2} U$:

Moreover, if we replace rule $r_2$ with $r_2'$ by swapping labels d and b in the right-hand side, then there is also a critical pair of shape $S \Rightarrow _{r_2'} T \Rightarrow _{r_1} U$. Indeed, this change makes the system non-terminating as the new critical pair is cyclic:

   $\square$

It is worth pointing out the mechanical nature of the termination proof in Example 3. Combining a simple label counting algorithm with a generator for sequential critical pairs would automatically determine that both rules are terminating and that there are no critical pairs of shape $S \Rightarrow _{r_2} T \Rightarrow _{r_1} U$. Based on Theorem 2, this method would then report that the combined system is terminating.

Fig. 9.

A terminating graph transformation system [5]

Example 4

The graph transformation system in Fig. 9 is shown to be terminating in [5]. The technique used is to first simplify the system by removing rules $r_3$ and $r_4$, obtaining a system that is terminating if and only if the original system is terminating. The argument is as follows: rule $r_3$ decreases the number of B-labels while no other rule increases this number. Hence any infinite derivation contains only finitely many applications of $r_3$ and thus $\langle \varSigma ,\{r_1,\dots ,r_4\}\rangle$ is terminating if and only if $\langle \varSigma ,\{r_1,r_2,r_4\}\rangle$ is terminating. After removing $r_3$, one can observe that rule $r_4$ reduces the number of R-labels while neither $r_1$ nor $r_2$ increase this number. Hence $r_4$ can be removed, too.

For the simplified system $\langle \varSigma ,\{r_1,r_2\}\rangle$, a so-called weighted type graph over the tropical semiring is constructed [5] which provides a decreasing measure for both rules. We can give a simpler termination argument for this system by using the approach of Example 3: $r_1$ is terminating as it reduces the number of 0’s and $r_2$ is terminating as it reduces the number of 1’s. Also, it is easy to check that there are no critical pairs of shape $S \Rightarrow _{r_1} T \Rightarrow _{r_2} U$ or $S \Rightarrow _{r_2} T \Rightarrow _{r_1} U$. Hence Theorem 2 guarantees that $\langle \varSigma ,\{r_1,r_2\}\rangle$ is terminating.    $\square$

Similar to Example 3, our termination proof could be found automatically by a tool that counts labels, eliminates rules that decrease label counts not increased by the other rules, and finally generates sequential critical pairs.

Example 5

The hypergraph transformation system in Fig. 10 checks, when applied as long as possible, whether a host graph is 2-colourable (bipartite). If this is the case, the rules colour the graph accordingly. We assume that the initial hypergraph is a loop-free connected graph in which each node has exactly one “colour flag” attached to it (a hyperedge e with $|\mathrm {att}_G(e)| = 1$). Moreover, exactly one flag should be labelled r (or b) and all other flags should be blank. To save space, we deviate from our usual drawing convention in that all ordinary edges shown in the rules are interface edges.

Fig. 10.

Hypergraph transformation system for generating a 2-colouring

If the initial graph is 2-colourable, the system of Fig. 10 will terminate with a coloured version of the graph in which each node is coloured r or b. (A graph is 2-colourable if its underlying undirected graph has no cycles of odd length.) If the graph is not 2-colourable, this will eventually be detected by the Invalid rules. The Propagate rules then make sure that all colour flags are black in the final graph.

As in the previous examples, we can prove termination of the system by label counting and Theorem 2. Subsystem Colour is terminating because all rules reduce the number of blank flags. On the other hand, $\mathrm {Invalid} \cup \mathrm {Propagate}$ is terminating as all rules decrease the number of non-black flags. It is easy to see that there are no critical pairs of shape $S \Rightarrow _{\mathrm {Invalid} \cup \mathrm {Propagate}} T \Rightarrow _{\mathrm {Colour}} U$ (since all ordinary edges are interface edges) and thus the combined system is terminating.    $\square$

We remark that termination of the system of Fig. 10 can alternatively be proved by removing the Colour rules and observing that the Invalid and Propagate rules reduce the number of non-black flags. This works because the Colour rules reduce the number of blank flags while the Invalid and Propagate rules do not increase this number. However, the point of Example 5 is to demonstrate that a non-trivial system can be decomposed into subsystems such that Theorem 2 is applicable, and where the components are proved terminating with different measures.

Example 6

Our final example is about jungle evaluation, a framework in which hypergraphs representing functional expressions are evaluated by transformation rules [12]. Figure 11 shows the non-injective evaluation rule corresponding to the term rewriting rule $\mathtt {y + 0} \rightarrow \mathtt {y}$, where the notation x=y means that interface nodes x and y are merged by the right-hand morphism. This rule is clearly terminating as it reduces the size of any hypergraph it is applied to. Rule copy in Fig. 12, on the other hand, enlarges any hypergraph it is applied to. The rule copies an occurrence of the constant 0 that is shared by two s-functions. The rule is terminating because each application reduces the measure

$$\begin{aligned} \#G = \sum _{v \in V_G} \mathrm {indegree}(v)^2. \end{aligned}$$

For, consider a step $G \Rightarrow _{\text {copy}} H$ and let n be the indegree of node z in G. Then $\#H = (\#G - n^2) + (n-1)^2 + 1 < \#G$ where the inequality holds because $(n-1)^2 + 1 < n^2$ for $n \ge 2$, and $n = \mathrm {indegree}(z) \ge 2$.

Fig. 11.

Jungle evaluation rule for $\mathtt {y + 0} \rightarrow \mathtt {y}$

Fig. 12.

Rule for copying a shared constant $\mathtt {0}$

It is not difficult to check that there are no sequential critical pairs of shape $S \Rightarrow _{\text {eval}} T \Rightarrow _{\text {copy}} U$, and thus the combined system $\{\text {eval},\,\text {copy}\}$ is terminating by Theorem 2. Note that it is not obvious how to combine graph size and the # value into a measure that decreases under rule applications of the combined rule set. This is because copy always increases graph size and eval increases the # value when applied to certain hypergraphs. To see the latter, consider a step $G \Rightarrow _{\text {eval}} H$ where $\mathrm {indegree}(x) = 2$, $\mathrm {indegree}(y) = 3$ and $\mathrm {indegree}(z) = 1$. Then $\#H = \#G - (4 + 9 + 1) + (4^2 - 1) = \#G + 1$.    $\square$

5 Conclusion and Future Work

Termination is an undecidable property of graph transformation systems. We have established a criterion based on the absence of certain sequential critical pairs which guarantees that the union of two terminating systems is terminating. This allows to split systems into component systems whose termination is then verified separately, possibly using different techniques, and to conclude that the combination of the components is terminating if the critical pair-criterion is satisfied. The criterion is syntactic and can be machine-checked by generating all critical pairs between rules from different component systems. Moreover, the method is a black-box approach in that the termination proofs of the component systems need not be inspected.

An obvious topic for future work is to implement a tool that given a hypergraph transformation system, generates all sequential critical pairs and calculates all possible partitions of the system into smaller components such that the condition of Theorem 2 is satisfied. For each partition, the components can then be proved to be terminating with whatever method seems suitable resp. has been implemented. The tool could be used together with a termination prover such as Grez, described in [5], which allows to choose different proof methods, including weighted type graphs, label counting and node counting.

Future research may also attempt to generalize Theorem 2 in various ways. It may be possible to allow critical pairs $S \Rightarrow _{\mathcal {R}} T \Rightarrow _{\mathcal {S}} U$ and formulate conditions under which arbitrary steps $G \Rightarrow _{\mathcal {R}} H \Rightarrow _{\mathcal {S}} M$ can still be swapped. A naive try is to require that there exits a graph $T'$ such that $S \Rightarrow _{\mathcal {S}} T' \Rightarrow _{\mathcal {R}} U$, which however is insufficient as the dangling condition may prevent embedding the steps into context. The situation has some similarity with the analysis of conventional critical pairs to verify confluence: the mere joinability of all critical pairs does not guarantee local confluence of a set of rules [20].

Finally, it would be desirable to extend the approach of this paper such that rules with application conditions (of some form) can be handled. Even more challenging is an extension to attributed graph transformation on which graph programming languages such as GP 2 are based. This is because finite sets of attributed rules typically induce infinite sets of sequential critical pairs in the sense of this paper (see [13] for the corresponding problem with conventional critical pairs).