Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings

TL;DR

This paper presents a novel framework for proving the termination of graph transformation systems by extending matrix interpretation techniques from string rewriting to graph rewriting using weighted type graphs over semirings.

Contribution

It generalizes matrix interpretation methods to graph rewriting and introduces a new variant of arithmetic type graphs over ordered semirings for termination proofs.

Findings

Framework successfully proves termination in example with counters

Implementation integrated into the Grez tool

Extends matrix interpretation techniques to graph rewriting

Abstract

We introduce techniques for proving uniform termination of graph transformation systems, based on matrix interpretations for string rewriting. We generalize this technique by adapting it to graph rewriting instead of string rewriting and by generalizing to ordered semirings. In this way we obtain a framework which is inspired by the tropical and arctic type graphs of [5] and introduces a new variant of arithmetic type graphs. These type graphs can be used to assign weights to graphs and to show that these weights decrease in every rewriting step in order to prove termination. We present an example involving counters and discuss the implementation in the tool Grez.