Refine
Document Type
- Article (9)
- Monograph/Edited Volume (2)
- Postprint (1)
Language
- English (12)
Is part of the Bibliography
- yes (12)
Keywords
- Nested graph conditions (2)
- nested graph conditions (2)
- verschachtelte Graphbedingungen (2)
- Algebraic methods (1)
- Application (1)
- Attributed graph transformation (1)
- Attributed graphs (1)
- Consistency (1)
- Critical pair analysis (1)
- Critical pairs (1)
- Delta preservation (1)
- Erfüllbarkeitsanalyse (1)
- Formal modelling (1)
- Graph databases (1)
- Graph logic (1)
- Graph logics (1)
- Graph queries (1)
- Graph repair (1)
- Graph transformation (1)
- Graphreparatur (1)
- Graphtransformation (1)
- Inheritance (1)
- Initial conflicts (1)
- Institutions (1)
- Konsistenzrestauration (1)
- M-adhesive categories (1)
- M-adhesive category with NACs (1)
- M-adhesive transformation systems (1)
- Model generation (1)
- Model repair (1)
- Model-driven (1)
- Modellerzeugung (1)
- Modellreparatur (1)
- Navigational logics (1)
- Specification (1)
- Tableau method (1)
- Tableaumethode (1)
- Typed attributed graph transformation (1)
- categories (1)
- conditions (1)
- confluence (1)
- consistency restoration (1)
- critical pairs (1)
- distributed systems (1)
- embedding (1)
- engineering (1)
- grammars (1)
- graph repair (1)
- graph replacement categories (1)
- graph transformation (1)
- graph-transformations (1)
- lazy transformation (1)
- level-replacement systems (1)
- local confluence (1)
- model (1)
- model generation (1)
- model repair (1)
- nested application conditions (1)
- programs (1)
- restoration (1)
- satisfiabilitiy solving (1)
- symbolic graph transformation (1)
- synchronization (1)
- tableau method (1)
Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update.
Nested application conditions generalise the well-known negative application conditions and are important for several application domains. In this paper, we present Local Church-Rosser, Parallelism, Concurrency and Amalgamation Theorems for rules with nested application conditions in the framework of M-adhesive categories, where M-adhesive categories are slightly more general than weak adhesive high-level replacement categories. Most of the proofs are based on the corresponding statements for rules without application conditions and two shift lemmas stating that nested application conditions can be shifted over morphisms and rules.
Graphs play an important role in many areas of Computer Science. In particular, our work is motivated by model-driven software development and by graph databases. For this reason, it is very important to have the means to express and to reason about the properties that a given graph may satisfy. With this aim, in this paper we present a visual logic that allows us to describe graph properties, including navigational properties, i.e., properties about the paths in a graph. The logic is equipped with a deductive tableau method that we have proved to be sound and complete.