
Abstract:
Using graph transformation as a formalism to specify model transformation, termination and confluence of the graph transformation system are required properties. Only under these two conditions, existence and uniqueness of the outcoming model is ensured. Verifying confluence of a graph transformation system is equivalent to checking both local confluence and termination. A graph transformation system is locally confluent, if all its conflicts in a minimal context can be resolved. Formally, this means, that all critical pairs of the graph transformation system should be strictly confluent. Thus, answering the question of local confluence of a graph transformation system, requires the following two steps. At first the computation of all critical pairs is necessary. Secondly, this set of critical pairs has to be tested for strict confluence. This paper concentrates on the first step, proposing an efficient method to compute the set of all critical pairs of a given graph transformation system. Efficiency is obtained, because of the following two main reasons. At first, all pairs of rules are analyzed to check, if they can actually cause a conflict. Then for each conflict inducing pair of rules, the set of critical pairs is computed in a constructive way, avoiding needless computations.
Keywords:
conflict, confluence, critical pair, graph transformation, Model transformation
BibTeX file
title = { Efficient Detection of Conflicts in Graph-Based Model Transformation },
year = { 2005 },
volume = { 152 },
pages = { 97--109 },
abstract = { Using graph transformation as a formalism to specify model transformation, termination and confluence of the graph transformation system are required properties. Only under these two conditions, existence and uniqueness of the outcoming model is ensured. Verifying confluence of a graph transformation system is equivalent to checking both local confluence and termination. A graph transformation system is locally confluent, if all its conflicts in a minimal context can be resolved. Formally, this means, that all critical pairs of the graph transformation system should be strictly confluent. Thus, answering the question of local confluence of a graph transformation system, requires the following two steps. At first the computation of all critical pairs is necessary. Secondly, this set of critical pairs has to be tested for strict confluence. This paper concentrates on the first step, proposing an efficient method to compute the set of all critical pairs of a given graph transformation system. Efficiency is obtained, because of the following two main reasons. At first, all pairs of rules are analyzed to check, if they can actually cause a conflict. Then for each conflict inducing pair of rules, the set of critical pairs is computed in a constructive way, avoiding needless computations. },
month = { 9 },
keywords = { conflict, confluence, critical pair, graph transformation, Model transformation },
publisher = { Elsevier Science },
series = { Electronic Notes in Theoretical Computer Science },
address = { Tallinn, Estonia },
booktitle = { Proc. International Workshop on Graph and Model Transformation (GraMoT'05) }
Copyright Notice
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
last change: Mon, 18 Jan 2010 15:27:02 +0100


