Termination Criteria for LGTS

In AGG termination criteria are implemented for Layered Graph Transformation Systems (LGTS) (see section 1.10). In general, termination is undecidable for graph grammars. But if the graph grammars meet suitable termination criteria, we can conclude that they are terminating. The criteria we propose are based on assigning a layer to each rule, node and edge type.
For termination, we define layered graph grammars with deletion and non-deletion layers. Termination criteria are expressed by deletion and nondeletion layer conditions.

A graph grammar is called layered graph grammar (LGG) if for each rule $r$ we have a rule layer $rl(r) = k$ and for each label $l$ a creation layer $cl(l)$ and a deletion layer $dl(l)$. The following conditions have to be satisfied for all rules:

(1) Deletion Layer Conditions
If $k$ is a deletion layer, then

1. each rule $r$ decreases the number of graph items, or
2. each rule $r$ decreases the number of graph items of one special type.

(2) Deletion Layer Conditions
If $k$ is a deletion layer, then

1. $r$ deletes at least one item,
2. $0 <= cl(l) <= dl (l) <= n$ for all $l$,
3. if $r$ deletes $l$ then $dl(l) <= rl(r)$,
4. if $r$ creates $l$ then $cl(l) > rl(r)$.

(3) Nondeletion Layer Conditions
If $k$ is a nondeletion layer, then

1. $r$ is nondeleting, i.e. $r : L -> R$ is total and injective,
2. $r$ has NAC $n : L -> N$ with $n' : N -> R$ injective s.t. $n'$ o $n = r$,
3. if $l$ occurs in $L$ then $cl(l) <= rl(r)$,
4. if $r$ creates $l$ then $cl(l) > rl(r)$.

The termination criterion (1) and (2) are a general termination criteria of typed layered graph transformation systems.
The termination criterion (3) is defined for typed graph transformation with injective rules, injective matches and injective negative application conditions (NACs).

The deletion layer conditions (2) ensure that the last creation of an element of a certain type always precedes the first deletion of an element of the same type.
On the other hand, nondeletion layer conditions (3) ensure that if an element of a certain type occurs in the LHS of a rule then all elements of the same type were already created in this or a previous layer. New elements have to have creation layers larger than the layer of the rule which creates them.

A layered graph grammar with deletion and nondeletion layers terminates, if for each layer the deletion or nondeletion layer conditions defined above are satisfied.
The rule layers can be set or generated. The creation and deletion type layers will be generated automatically s.th. for each layer one set of layer conditions is satisfied, if this is possible.

The graphical user interface to define rule, creation and deletion layers is available by menu item Analyzer/Termination Check and shown in Figure 65. There, the rules and user-defined rule layers of our example StateCharts are shown.

Figure 65: Termination dialog

Figure 66 shows the generated creation and deletion layers for types in addition. Moreover, we can see that the termination criteria are fulfilled by these layer assignments.

Figure 66: Termination dialog

A layered graph grammar with deletion and nondeletion layers terminates, if for each layer the deletion and nondeletion layer conditions defined above are satisfied.

Termination criteria are described in:

• ''Termination Criteria for Model Transformation'' by H. Ehrig, K. Ehrig, J. de Lara, G. Taentzer, D. Varro, and S. Varro-Gyapay (http://www.cs.tu-berlin.de/~ehrig/public/EEL+05.pdf).
• ''Termination of High-Level Replacement Units with Application to Model Transformation'' by P. Bottoni, M. Koch, F. Parisi-Presicce, and G. Taentzer (http://tfs.cs.tu-berlin.de/agg/BotKocParTaeENTCS.pdf).