Improving conflict detection in double-pushout graph transformation

Abstract

Graph transformation is a useful framework for the specification, analysis and development of software, particularly within Model-Driven methodologies. In this setting, graphs or graph-like structures are used to represent states of a system, while its possible transitions are determined by transformation rules. This combines an intuitive visual representation with a rich theory and several verification techniques. Since the behaviour of these a rule-based models emerges from the interactions between rules, techniques for understanding such interactions are necessary. In this work, we focus on conflicts: situations where the application of a rule hinders the application of another. Conflict detection is then a static analysis technique that enumerates a finite but complete set of such situations, in the sense that every other conflict can be expressed in terms of some detected conflict. The most common approach to conflict detection is the enumeration of so-called critical pairs, and it was successfully applied in several contexts. Nevertheless, it still faces some issues related to scalability. These involve the running time of existing algorithms, but more fundamentally they stem from the amount of redundant potential conflicts that are enumerated. In this work, we take an important step towards improving conflict detection and reducing the redundancy of results. To this end, we develop a theory describing the root causes of conflicts in the form of conflict essences. Using lattice-theoretical techniques, we were also able to detect further sources of redundancy, identifying irreducible essences as suitable, less redundant subset. We also show that conflict essences are closely related to initial conflicts, a recently proposed subset of critical pairs, allowing their application to a wider variety of contexts. Moreover, simple algorithms for enumerating conflict and irreducible essences are provided. Finally, we present experimental evidence that initial conflicts and irreducible essences allow a significant reduction on the number of reported conflicts, when compared to the more traditional critical pairs, without loss of information. All of our results hold for categories of set-valued functors, a generalisation of graphs and graph structures, and sufficient conditions are identified for most of our results to hold in other adhesive categories.

Transformação de grafos é uma teoria apropriada para a especificação, análise e desenvolvimento de software, particularmente em abordagens dirigidas a modelos. Nesse contexto, grafos ou estruturas semelhantes representam os estados de um sistema, enquanto as transições são determinadas por regras de reescrita. Assim, uma representação visual e intuitiva é combinada a uma vasta teoria, permitindo o uso de várias técnicas de verificação. Como o comportamento desses modelos baseados em regras emerge de suas interações, são necessárias técnicas para entendê-las. Nesse trabalho, focamos nos conflitos entre regras: situações em que a aplicação de uma regra impede a aplicação de outra. A análise estática denominada detecção de conflitos busca enumerar um conjunto finito dessas situações que seja completo, ou seja, tal que qualquer outro conflito possa ser expresso em termos de um dos conflitos detectados. Em particular, a enumeração de pares críticos foi aplicada com sucesso em vários contextos. Ainda assim, a ela encontra problemas relacionados à escalabilidade. Isso envolve o tempo de execução, mas fundamentalmente advém do grande número de conflitos potenciais redundantes que é identificado. Neste trabalho, damos um passo importante em direção a uma técnica mais eficiente para detecção de conflitos. Para isso, desenvolvemos uma teoria que descreve a causa principal dos conflitos na forma de essências de conflito. Usando teoria de reticulados, pudemos detectar mais fontes de redundância, identificando essências irredutíveis como um subconjunto apropriado e menos redundante. Também mostramos que essas são intimamente relacionadas aos conflitos iniciais, um subconjunto dos pares críticos proposto recentemente. Assim, a aplicação de conflitos iniciais se torna possível em novos contextos. Além disso, apresentamos algoritmos para enumerar essências de conflito, conflitos iniciais e essências irredutíveis. Por fim, apresentamos evidência empírica de que conflitos iniciais e essências irredutíveis reduzem significativamente o número de conflitos reportados, em relação aos pares críticos, sem perda de informação. Todos os resultados teóricos deste trabalho são válidos para categorias de funtores com codomínio na categoria de conjuntos, uma generalização de grafos e de graph structures. Também identificamos condições suficientes para que os principais resultados sejam válidos em outras categorias adesivas.