February 17, 2014MSc Presentation: Conflict Detection and Analysis for Single-Pushout High-Level Replacement
Room: Ra 2231Ruud Welling

In many graph transformation systems (local) confluence is a desired property. For instance, if graph transformation is used for model transformation, then confluence and termination ensure that the order in which rules are applied does not matter, in other words, the nal result will always be the same.

In this research we investigate sucient conditions for local confluence of high-level replacement (HLR) systems. Using the single-pushout high-level replacement approach we de ne critical pairs (minimal conflicting situations). Our sufficient condition for local confluence is based on the analysis of critical pairs. We provide our proofs on a categorical level, therefore our theory cannot only be applied to the category of graphs: we formulate requirements for the categories for which our theorems hold, and we show that our theory is also applicable to attributed graphs.

We also present some of the foundations for confluence analysis for HLR systems with negative application conditions (NACs). In order to show local confluence for a HLR system with NACs we will show that stricter conditions must hold for the critical pairs with NACs (compared to the situation without NACs). We show that HLR systems without NACs are locally confluent. Further analysis of HLR systems with NACs is future work.

Our theory has been implemented in the graph transformation tool GROOVE. Using our implementation we can nd all critical pairs for a graph transformation system, and analyse if these pairs are locally confluent. Using this implementation we have performed some experiments on existing graph transformation systems.


project description