TY - JOUR A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - A logic-based incremental approach to graph repair featuring delta preservation JF - International journal on software tools for technology transfer : STTT N2 - We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain. KW - Nested graph conditions KW - Graph repair KW - Model repair KW - Consistency KW - restoration KW - Delta preservation KW - Graph databases KW - Model-driven KW - engineering Y1 - 2021 U6 - https://doi.org/10.1007/s10009-020-00584-x SN - 1433-2779 SN - 1433-2787 VL - 23 IS - 3 SP - 369 EP - 410 PB - Springer CY - Berlin ; Heidelberg ER - TY - JOUR A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - Automated reasoning for attributed graph properties JF - International Journal on Software Tools for Technology Transfer N2 - Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation. KW - Attributed graphs KW - Nested graph conditions KW - Model generation KW - Tableau method KW - Graph queries Y1 - 2018 U6 - https://doi.org/10.1007/s10009-018-0496-3 SN - 1433-2779 SN - 1433-2787 VL - 20 IS - 6 SP - 705 EP - 737 PB - Springer CY - Heidelberg ER -