Initial conflicts and dependencies: Critical pairs revisited

Abstract

Considering a graph transformation system, a critical pair represents a pair of conflicting transformations in a minimal context. A conflict between two direct transformations of the same structure occurs if one of the transformations cannot be performed in the same way after the other one has taken place. Critical pairs allow for static conflict and dependency detection since there exists a critical pair for each conflict representing this conflict in a minimal context. Moreover it is sufficient to check each critical pair for strict confluence to conclude that the whole transformation system is locally confluent. Since these results were shown in the general categorical framework of M-adhesive systems, they can be instantiated for a variety of systems transforming e.g. (typed attributed) graphs, hypergraphs, and Petri nets. In this paper, we take a more declarative view on the minimality of conflicts and dependencies leading to the notions of initial conflicts and initial dependencies. Initial conflicts have the important new characteristic that for each given conflict a unique initial conflict exists representing it. We introduce initial conflicts for M-adhesive systems and show that the Completeness Theorem and the Local Confluence Theorem still hold. Moreover, we characterize initial conflicts for typed graph transformation systems and show that the set of initial conflicts is indeed smaller than the set of essential critical pairs (a first approach to reduce the set of critical pairs to the important ones). Dual results hold for initial dependencies.