Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Termination of Graph Transformation Systems Using Weighted Subgraph Counting

Roy Overbeek, Jörg Endrullis

TL;DR

A termination method for the algebraic graph transformation framework PBPO+, in which it is shown that toposes are naturally encodable into PBPO+ in the quasitopos setting and is applicable to non-linear rules.

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.

Termination of Graph Transformation Systems Using Weighted Subgraph Counting

TL;DR

A termination method for the algebraic graph transformation framework PBPO+, in which it is shown that toposes are naturally encodable into PBPO+ in the quasitopos setting and is applicable to non-linear rules.

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.
Paper Structure (22 sections, 24 theorems, 16 equations, 1 figure)

This paper contains 22 sections, 24 theorems, 16 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Basic Notions
  4. Termination
  5. Background
  6. Quasitoposes
  7. PBPO+
  8. Decreasingness by Counting Weighted Elements
  9. Relating Rule and Step
  10. Determining the Weight of the Pattern
  11. Sliding Tiles Injectively
  12. The Main Result
  13. Examples
  14. Related Work
  15. Implementation
  16. ...and 7 more sections

Key Result

Lemma 2.3

Assume the right square of is a pullback and the left square commutes. Then the outer rectangle (obtained by composing the horizontal morphisms) is a pullback iff the left square is a pullback. ∎

Figures (1)

  • Figure 1: Implications between (quasi)toposes and adhesivity properties.

Theorems & Definitions (83)

  • Remark 1.1
  • Definition 2.2: $\mathcal{A}$-Local Finiteness
  • Lemma 2.3: Pullback Lemma borceux1994handbook1
  • Definition 2.4: Split Epimorphism
  • Proposition 2.5: adamek2009joy
  • Definition 2.6: Graph Notions
  • Definition 2.7: ehrig2006fundamentals
  • Definition 2.8: DPO Rewriting ehrig1973graph
  • Definition 2.9
  • Definition 2.10
  • ...and 73 more