Confluence up to Garbage in Graph Transformation

TL;DR

This paper introduces the concept of confluence up to garbage in graph transformation systems, providing theoretical tools to analyze and ensure confluence on relevant graph subclasses despite non-confluence in general.

Contribution

It generalizes the critical pair lemma for double-pushout graph transformation to include confluence up to garbage, with practical case studies on language recognition.

Findings

Defined confluence up to garbage for graph transformations.

Extended critical pair analysis to non-confluent systems that are confluent on relevant subclasses.

Applied theory to graph reduction systems recognizing specific graph classes.

Abstract

The transformation of graphs and graph-like structures is ubiquitous in computer science. When a system is described by graph-transformation rules, it is often desirable that the rules are both terminating and confluent so that rule applications in an arbitrary order produce unique resulting graphs. However, there are application scenarios where the rules are not globally confluent but confluent on a subclass of graphs that are of interest. In other words, non-resolvable conflicts can only occur on graphs that are considered as "garbage". In this paper, we introduce the notion of confluence up to garbage and generalise Plump's critical pair lemma for double-pushout graph transformation, providing a sufficient condition for confluence up to garbage by non-garbage critical pair analysis. We apply our results in two case studies about efficient language recognition: we present backtracking-free graph reduction systems which recognise a class of flow diagrams and a class of labelled series-parallel graphs, respectively. Both systems are non-confluent but confluent up to garbage. We also give a critical pair condition for subcommutativity up to garbage which, together with closedness, implies confluence up to garbage even in non-terminating systems.