GReTA seminar #5: "Confluence of Graph Transformation"
Channel: GReTA Seminar
Date: 2021-01-29

Speakers: Leen Lambers (Hasso-Plattner-Institut Potsdam, Germany) & Fernando Orejas (Technical University of Catalonia (UPC), Spain)

Abstract:

Confluence has been studied for graph transformation since several decades now.  Confluence analysis has been applied, for example, to determining uniqueness of model transformation results in model-driven engineering.  It is strongly related to conflict analysis for graph transformation, i.e. detecting and inspecting all possible conflicts that may occur for a given set of graph transformation rules. The latter finds applications, for example, in software analysis and design.  Both conflict and confluence analysis rely on the existence and further analysis of a finite and representative set of conflicts for a given set of graph transformation rules.

Traditionally, the set of critical pairs has been shown to constitute such a set. It is representative in the sense that for each conflict a critical pair exists, representing the conflict in a minimal context, such that it can be extended injectively to this conflict (M-completeness). Recently, it has been shown that initial conflicts constitute a considerably reduced subset of critical pairs, being still representative in a slightly different way.  In particular, for each conflict there exists a unique initial conflict that can be extended (possibly non-injectively) to the given conflict (completeness).  Compared to the set of critical pairs, the smaller set of initial conflicts allows for more efficient conflict as well as confluence analysis.

We continue by demonstrating that initial conflicts (critical pairs) are minimally complete (resp. minimally M-complete), and thus are both optimally reduced w.r.t. representing conflicts in a minimal context via general (resp. injective) extension morphisms. We proceed with showing that it is impossible to generalize this result to the case of rules with application conditions (equivalent to FOL on graphs).  We therefore revert to a symbolic setting, where finiteness and minimal (M-)completeness can again be guaranteed.  Finally, we describe important special cases (e.g. rules with negative application conditions), where we are able to obtain minimally complete (resp. M-complete) sets of conflicts in the concrete setting again.

About the GReTA seminars:

The GReTA – Graph TRansformation Theory and Applications virtual seminar series aims to serve as a platform for the international graph rewriting community, to promote recent developments and trends in the field, and to permit a regular networking and interaction between members of this community. Seminars are held twice a month in the form of Zoom sessions (some of which will be live-streamed to YouTube). Please refer to http://www.irif.fr/~greta for further details (including information on how to register for participating in the Zoom meetings).