Roy Overbeek ; Jörg Endrullis - Termination of Graph Transformation Systems Using Weighted Subgraph Counting

lmcs:12700 - Logical Methods in Computer Science, November 12, 2024, Volume 20, Issue 4 - https://doi.org/10.46298/lmcs-20(4:12)2024
Termination of Graph Transformation Systems Using Weighted Subgraph CountingArticle

Authors: Roy Overbeek ; Jörg Endrullis

    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.


    Volume: Volume 20, Issue 4
    Published on: November 12, 2024
    Accepted on: September 4, 2024
    Submitted on: December 18, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 582 times.
    This article's PDF has been downloaded 309 times.