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.

翻译：我们提出了基于矩阵解释的字符串重写技术，用于证明图变换系统的统一终止性。通过将这一技术从字符串重写推广到图重写，并进一步推广到有序半环，我们获得了受[5]中热带与北极类型图启发的框架，同时引入了算术类型图的新变体。这些类型图可用于为图分配权重，并通过证明每次重写步骤中权重递减来验证终止性。本文给出了一个包含计数器的示例，并讨论了该技术在Grez工具中的实现。