一句话：提出通过加权子图计数证明 PBPO+ 图变换系统终止性的方法，支持非线性规则并推广到 SqPO 与左线性 DPO。
本文研究代数图变换系统（如 PBPO+）的终止性证明问题，尤其针对非线性规则和现有方法难以覆盖的框架。作者提出加权子图计数方法：通过对指向对象的加权态射类求和来为对象赋权，并据此构造终止度量；该方法在 rm-adhesive quasitoposes（包含 topos 及许多图范畴）中良定义。由于 SqPO 与左线性 DPO 可自然编码到准拓扑斯设置下的 PBPO+，该方法也适用于它们。作者实现了该技术，并提供 REPL 以辅助相对终止证明。
We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which include toposes and therefore many graph categories of interest), and is applicable to non-linear rules. The method is also defined for other frameworks, including SqPO and left-linear DPO, because we have previously shown that they are naturally encodable into PBPO+ in the quasitopos setting. We have implemented our method, and the implementation includes a REPL that can be used for guiding relative termination proofs.
@article{paperbot2711,
title = {Termination of Graph Transformation Systems Using Weighted Subgraph Counting},
author = {Roy Overbeek and Jörg Endrullis},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:12)2024}
}