Termination of Graph Transformation Systems via Generalized Weighted Type Graphs

TL;DR

The weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems is refined, the power of the approach for graphs is increased, and the technique is generalized to other categories.

Abstract

We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.

Figures (1)

• Figure 1: Causes of $\mathbf{w}_{}(C - u) \cdot \mathbf{w}_{}(L)$ overestimating the weight $\mathbf{w}_{}(G)$ of $G$.

Theorems & Definitions (8)

• proof
• proof
• proof
• proof
• proof
• proof
• proof : Proof of Theorem \ref{['thm:steps']}
• proof : Proof of Theorem \ref{['thm:termination']}