Confluence of Graph Transformation

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.

Date
Friday, January 29, 2021 15:00 Europe/Paris
Event
GReTA seminar
Leen Lambers
Leen Lambers
Professor of Computer Science

Leen Lambers is a professor of Software Systems Engineering at the Brandenburgische Technische Universität (BTU) Cottbus-Senftenberg. Previously, she was a senior researcher in the group System Analysis and Modeling (Prof. Holger Giese) at the Hasso Plattner Institute, University of Potsdam in Germany. Her main research area is quality assurance for data- and software-intensive systems with increasing adaptivity requirements. In particular, she focuses on modeling and analysis using graph transformation and graph logic. She has spent research periods in the Laboratory of Software Testing and Analysis (founded by Prof. Mauro Pezzé) at the University of Milano Bicocca and in the computer science department of the Technical University of Catalonia with Prof. Fernando Orejas. She served as PC member/chair for several international workshops and conferences related to quality assurance in software and systems engineering. She received a PhD for her dissertation “Certifying Rule-Based Models using Graph Transformation” (supervised by Prof. Hartmut Ehrig) at the Technical University of Berlin in 2009.

Fernando Orejas
Fernando Orejas
Professor of Computer Science

Member of the ALBCOM Research Group of the Department of Computer Science, Technical University of Catalonia, in Barcelona. (These are the English translations of Departament de Ciències de la Computació and Universitat Politècnica de Catalunya.)