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 DPO and SqPO, because we have previously shown that they are naturally encodable into PBPO+ in the quasitopos setting.
翻译:我们提出了一种针对代数图变换框架PBPO+的终止性判定方法,该方法通过对目标对象的加权态射类进行求和来度量对象权重。该判定方法在rm-黏合拟拓扑范畴(包含拓扑斯范畴及多数目标图范畴)中具有良定义性,适用于非线性规则。此方法同样适用于DPO和SqPO等其他框架,因为我们先前已证明在拟拓扑范畴设定下,这些框架可自然地编码为PBPO+形式。