Termination of Graph Transformation Systems Using Weighted Subgraph Counting
Logic in Computer Science
2024-11-13 v8
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.
Keywords
Cite
@article{arxiv.2303.07812,
title = {Termination of Graph Transformation Systems Using Weighted Subgraph Counting},
author = {Roy Overbeek and Jörg Endrullis},
journal= {arXiv preprint arXiv:2303.07812},
year = {2024}
}