Using weakest application conditions to rank graph transformations for graph repair
Lars Fritsche, Alexander Lauer, Maximilian Kratz, Andy Schürr, Gabriele Taentzer
TL;DR
The paper introduces a dynamic framework to rank graph-transformations by their potential to repair inconsistencies, using impairment- and repair-indicating application conditions derived from nested graph constraints. A central theorem connects the gain in consistency to the difference between repairs and impairments, enabling look-ahead and greedy optimization for graph repair. The approach is instantiated on the CRA problem, implemented in eMoflon, and evaluated against an ILP-based GIPS baseline, demonstrating scalable performance and competitive solution quality. The work extends prior constraint-checking and repair techniques by accommodating arbitrary nested constraints and providing a principled, weakest-direct-conditions characterization for consistency-preserving transformations.
Abstract
When using graphs and graph transformations to model systems, consistency is an important concern. While consistency has primarily been viewed as a binary property, i.e., a graph is consistent or inconsistent with respect to a set of constraints, recent work has presented an approach to consistency as a graduated property. This allows living with inconsistencies for a while and repairing them when necessary. For repairing inconsistencies in a graph, we use graph transformation rules with so-called {\em impairment-indicating and repair-indicating application conditions} to understand how much repair gain certain rule applications would bring. Both types of conditions can be derived from given graph constraints. Our main theorem shows that the difference between the number of actual constraint violations before and after a graph transformation step can be characterised by the difference between the numbers of violated impairment-indicating and repair-indicating application conditions. This theory forms the basis for algorithms with look-ahead that rank graph transformations according to their potential for graph repair. An evaluation shows that graph repair can be well-supported by rules with these new types of application conditions in terms of effectiveness and scalability.
