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.

翻译：我们针对代数图变换框架PBPO+引入了一种终止性判定方法，该方法通过求和针对目标对象的一类加权态射来对对象进行加权。该方法在rm-粘合拟拓扑（包含拓扑斯结构，因此涵盖众多有研究价值的图范畴）中定义良好，并且适用于非线性规则。由于我们先前已证明在拟拓扑环境下，包括SqPO和左线性DPO在内的其他框架可自然地编码为PBPO+，因此该方法同样适用于这些框架。我们已实现了该方法，其实现包含一个可用于指导相对终止性证明的交互式编程环境（REPL）。