Sven Schneider-Winden Book order

Graph repair, the process of restoring a graph's consistency, is essential in various fields of computer science. In model-driven engineering, for instance, the abstract syntax of models is often represented using graphs. Flexible editing operations can lead to temporary inconsistencies, necessitating graph repair. Similarly, in graph databases, updates might violate integrity constraints, prompting the need for repair. We propose a logic-based incremental approach to graph repair, providing a comprehensive overview of least-changing repairs that is sound and complete upon termination. Consistency is formalized through graph conditions equivalent to first-order logic on graphs. Our approach includes two types of repair algorithms: state-based repair, which restores consistency without regard to the update history, and delta-based repair, which considers this history explicitly. Our algorithms build on an existing model generation algorithm for graph conditions implemented in AutoGraph. Additionally, the delta-based method introduces satisfaction (ST) trees to represent how a graph meets a graph condition. We demonstrate the incremental manipulation of these STs in response to graph updates, highlighting the effectiveness of our approach in maintaining graph consistency.

Graphen sind in der Informatik allgegenwärtig, weshalb Methoden zur Darstellung und Untersuchung von Grapheigenschaften von großer Bedeutung sind. Besonders wichtig ist die vollautomatische Überprüfung der Erfüllbarkeit von Grapheigenschaften. In vielen Anwendungsszenarien ist es zudem wünschenswert, Graphen zu identifizieren, die bestimmte Eigenschaften erfüllen. Bei einer unendlichen Anzahl solcher Graphen ist ein kompakter Überblick anzustreben. Die Tableau-Methode für Grapheigenschaften von Lambers und Orejas ermöglicht die Entwicklung eines Algorithmus zur Generierung symbolischer Modelle. Grapheigenschaften werden in einer speziellen Logik formuliert, die auf Graphen und Graphmorphismen basiert und äquivalent zur First-Order Logic auf Graphen ist, wie sie von Courcelle eingeführt wurde. Der parallelisierbare Algorithmus ermittelt schrittweise eine endliche Menge symbolischer Modelle, wobei jedes Modell eine Menge endlicher Graphen beschreibt, die eine bestimmte Grapheigenschaft erfüllen. Diese Modelle gewährleisten Vollständigkeit, da sie alle endlichen Modelle abdecken, die die Eigenschaft erfüllen, und Korrektheit, da sie keine Graphen beschreiben, die die Eigenschaft verletzen. Zudem ist die Kompaktheit gegeben, da kein Modell von einem anderen abgedeckt wird. Der Algorithmus kann aus jedem symbolischen Modell ein minimales endliches Modell extrahieren und weitere endliche Modelle ableiten. Implementiert ist der Algor