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+，因此本方法同样适用于这些框架。我们已实现该方法，该实现包含可用于指导相对终止性证明的交互式解释环境。