Termination Criteria for LGTS

In  AGG  termination criteria are implemented for Layered Graph Transformation Systems (LGTS).
Termination of the rule applying of a certain layer is not always guaranteed.   The following conditions have to be satisfied for all rules.

For each rule   r   we have a rule layer   rl (r)   with  0 <= rl (r) <= k0   ( rl (r) , k0 in IN ), where   k0 + 1   is the number of layers, and for each label   l   a creation layer   cl (l) in IN   and a deletion layer   dl (l) in IN .

(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 rule layer   k   is a deletion layer, then
1. r   deletes at least one item,
2. 0 <= cl (l) <= dl (l) <= k0   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 rule layer   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   x   with   type(x) = l   occurs in   L   then   cl (l) <= rl (r) ,
4. if   r   creates an item of type   l   then   cl (l) > rl (r) .

The termination criteria (2) and (3) are 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 should precede 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.

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

In  AGG,  the rule layer can be set or generated. The creation and deletion type layer will be generated automatically. For each layer one set of layer conditions will be proved.