Confluence of typed attributed graph transformation systems

The issue of confluence is of major importance for the successful application of attributed graph transformation, such as automated translation of UML models into semantic domains. Whereas termination is undecidable in general and must be established by carefully designing the rules, local confluence can be shown for term rewriting and graph rewriting using the concept of critical pairs. In this paper, we discuss typed attributed graph transformation using a new simplified notion of attribution. For this kind of attributed graph transformation systems we establish a definition of critical pairs and prove a critical pair lemma, stating that local confluence follows from confluence of all critical pairs.