An algorithm for the critical pair analysis of amalgamated graph transformations

Abstract

Graph transformation has been shown to be well suited as formal foundation for model transformations. While simple model changes may be specified by simple transformation rules, this is usually not sufficient for more complex changes. In these situations, the concept of amalgamated transformation has been increasingly often used to model for each loops of rule applications which coincide in common core actions. Such a loop can be specified by a kernel rule and a set of extending multi-rules forming an interaction scheme. The Critical Pair Analysis (CPA) can be used to show local confluence of graph transformation systems. Each critical pair reports on a potential conflict between two rules. It has been shown recently that the generally infinite set of critical pairs for interaction schemes can be reduced to a finite set of non-redundant pairs being sufficient to show local confluence of the transformation system. Building on this basic result, we present an algorithm that is able to compute all non-redundant critical pairs for two given interaction schemes. The algorithm is implemented for Henshin, a model transformation environment based on graph transformation concepts.