Termination of Graph Transformation Systems Using Weighted Subgraph Counting

Abstract

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.

References in corpus (5)

• Compositional Scientific Computing with Catlab and SemanticModels
• Graph Rewriting and Relabeling with PBPO+: A Unifying Theory for Quasitoposes
• A PBPO+ Graph Rewriting Tutorial
• Kruskal's Tree Theorem for Acyclic Term Graphs
• From Linear Term Rewriting to Graph Rewriting with Preservation of Termination