2024

  1. Termination of Graph Transformation Systems Using Weighted Subgraph Counting
    Roy Overbeek, and Jörg Endrullis
    Log. Methods Comput. Sci. , 20 (4) (2024)
    paper

    Summary

    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.

    This paper is an extended version of Termination of Graph Transformation Systems Using Weighted Subgraph Counting (ICGT 2023).

    Bibtex

    @article{graph:termination:subgraph:counting:2024,
      author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
      title = {Termination of Graph Transformation Systems Using Weighted Subgraph
                        Counting},
      journal = {Log. Methods Comput. Sci.},
      volume = {20},
      number = {4},
      year = {2024},
      url = {https://doi.org/10.46298/lmcs-20(4:12)2024},
      doi = {10.46298/LMCS-20(4:12)2024},
      biburl = {https://dblp.org/rec/journals/lmcs/OverbeekE24.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org},
      keywords = {rewriting, termination},
      type = {journal}
    }
    

    Digital Object Identifier

    10.46298/LMCS-20(4:12)2024
  2. Correspondence Between Composite Theories and Distributive Laws
    RossetAloı̈s, Maaike Zwart, Helle Hvid Hansen, and Jörg Endrullis
    In: Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Proceedings König, Barbara and Urbat, Henning (eds.) , pp. 194–215 , Springer (2024)
    paper

    Summary

    Composite theories are the algebraic equivalent of distributive laws. In this paper, we delve into the details of this correspondence and concretely show how to construct a composite theory from a distributive law and vice versa. Using term rewriting methods, we also describe when a minimal set of equations axiomatises the composite theory.

    Bibtex

    @inproceedings{monads:composite:theories:2024,
      author = {Rosset, Alo{\"{\i}}s and Zwart, Maaike and Hansen, Helle Hvid and Endrullis, J{\"{o}}rg},
      editor = {K{\"{o}}nig, Barbara and Urbat, Henning},
      title = {Correspondence Between Composite Theories and Distributive Laws},
      booktitle = {Coalgebraic Methods in Computer Science - 17th {IFIP} {WG} 1.3 International
                        Workshop, {CMCS} 2024, Colocated with {ETAPS} 2024, Luxembourg City,
                        Luxembourg, April 6-7, 2024, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {14617},
      pages = {194--215},
      publisher = {Springer},
      year = {2024},
      url = {https://doi.org/10.1007/978-3-031-66438-0\_10},
      doi = {10.1007/978-3-031-66438-0\_10},
      biburl = {https://dblp.org/rec/conf/cmcs/RossetZHE24.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org},
      keywords = {coalgebra, rewriting},
      type = {workshop}
    }
    

    Digital Object Identifier

    10.1007/978-3-031-66438-0_10
  3. Generalized Weighted Type Graphs for Termination of Graph Transformation Systems
    Jörg Endrullis, and Roy Overbeek
    In: Graph Transformation - 17th International Conference, ICGT 2024, Held as Part of STAF 2024, Enschede, The Netherlands, July 10-11, 2024, Proceedings Harmer, Russ and Kosiol, Jens (eds.) , pp. 39–58 , Springer (2024)
    paper

    Summary

    We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.

    An extended version appeared as Termination of Graph Transformation Systems via Generalized Weighted Type Graphs (LMCS 2026).

    Bibtex

    @inproceedings{graph:termination:type:graphs:2024,
      author = {Endrullis, J{\"{o}}rg and Overbeek, Roy},
      editor = {Harmer, Russ and Kosiol, Jens},
      title = {Generalized Weighted Type Graphs for Termination of Graph Transformation
                        Systems},
      booktitle = {Graph Transformation - 17th International Conference, {ICGT} 2024,
                        Held as Part of {STAF} 2024, Enschede, The Netherlands, July 10-11,
                        2024, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {14774},
      pages = {39--58},
      publisher = {Springer},
      year = {2024},
      url = {https://doi.org/10.1007/978-3-031-64285-2\_3},
      doi = {10.1007/978-3-031-64285-2\_3},
      biburl = {https://dblp.org/rec/conf/gg/EndrullisO24.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org},
      keywords = {rewriting, termination},
      type = {conference}
    }
    

    Digital Object Identifier

    10.1007/978-3-031-64285-2_3