一句话：改进并推广加权类型图方法，证明更广的DPO图变换系统及变体的终止性。
本文研究双推出（DPO）图变换系统的终止性证明问题。作者改进加权类型图技术：一方面增强其在图上的证明能力，另一方面将方法推广到更一般的范畴，并使其适用于文献中出现的多种DPO变体。方法通过构造加权类型图，为重写规则赋予满足兼容性的权重，进而导出排除无限归约的良基度量。论文给出推广后技术的定义与适用条件，并说明其如何统一和扩展现有结果。关键结果是，该广义框架能处理更广的图变换系统及变体，从而提升终止性自动证明的覆盖范围。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{EndrullisO26,
title = {Termination of Graph Transformation Systems via Generalized Weighted Type Graphs},
author = {Jörg Endrullis and Roy Overbeek},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:15)2026}
}