2026

  1. Decreasing Diagrams Are Complete for Confluence
    Jörg Endrullis, Ievgen Ivanov, and Femke van Raamsdonk
    https://arxiv.org/abs/2610.06368, (2026)
    paper

    Summary

    The decreasing diagrams technique of van Oostrom is one of the most versatile methods for establishing confluence of transition systems (abstract rewriting systems). It reduces global confluence to local confluence: a system is confluent whenever its transitions admit a locally decreasing labeling.

    A central question, posed by van Oostrom in 1993, asks whether the decreasing diagrams technique is complete: does every confluent transition system admit a locally decreasing labeling? This is Problem 56 of the RTA List of Open Problems. We prove that every confluent transition system admits a locally decreasing labeling using only three labels. This bound is optimal, as two labels do not suffice even at the first uncountable cardinality. The entire development is machine-checked in the Isabelle/HOL and Lean proof assistants (Zenodo).

    See research for an overview of my research on confluence.

    Bibtex

    @misc{confluence:decreasing:diagrams:2026,
  author = {Endrullis, J{\"{o}}rg and Ivanov, Ievgen and van Raamsdonk, Femke},
  title = {Decreasing Diagrams are Complete for Confluence},
  howpublished = {arXiv preprint 2610.06368},
  year = {2026},
  url = {https://arxiv.org/abs/2610.06368},
  doi = {10.48550/arXiv.2610.06368},
  keywords = {rewriting, confluence},
  type = {miscellaneous}
}

    Digital Object Identifier

    10.48550/arXiv.2610.06368
  2. Termination of Graph Transformation Systems via Generalized Weighted Type Graphs
    Jörg Endrullis, and Roy Overbeek
    Log. Methods Comput. Sci. , 22 (1) (2026)
    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.

    This paper is an extended version of Generalized Weighted Type Graphs for Termination of Graph Transformation Systems (ICGT 2024).

    Bibtex

    @article{graph:termination:type:graphs:2026,
  author = {Endrullis, J{\"{o}}rg and Overbeek, Roy},
  title = {Termination of Graph Transformation Systems via Generalized Weighted
                    Type Graphs},
  journal = {Log. Methods Comput. Sci.},
  volume = {22},
  number = {1},
  year = {2026},
  url = {https://doi.org/10.46298/lmcs-22(1:15)2026},
  doi = {10.46298/LMCS-22(1:15)2026},
  biburl = {https://dblp.org/rec/journals/lmcs/EndrullisO26.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {journal}
}

    Digital Object Identifier

    10.46298/LMCS-22(1:15)2026