Termination of Injective DPO Graph Rewriting Systems using Subgraph Counting with anti-patterns
Qi Qiu · HAL (Le Centre pour la Communication Scientifique Directe) · 2025
A machine-checkable sufficient condition for relative termination of double-pushout graph rewriting systems with injective rules on edge-labeled multigraphs is presented. It defines a graph's weight as the sum of weights of occurrences of a set of graphs within that graph. It resolves termination cases that prior interpretation-based methods cannot. An implementation 1 is also provided.