@book{SchneiderLambersOrejas2019,
  author    = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
  title     = {A logic-based incremental approach to graph repair},
  number    = {126},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-462-3},
  issn      = {1613-5652},
  doi       = {10.25932/publishup-42751},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-427517},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {34},
  year      = {2019},
  abstract  = {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.},
  language  = {en}
}
@book{GieseMaximovaSakizloglouetal.2018,
  author    = {Giese, Holger and Maximova, Maria and Sakizloglou, Lucas and Schneider, Sven},
  title     = {Metric temporal graph logic over typed attributed graphs},
  number    = {123},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-433-3},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-411351},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {29},
  year      = {2018},
  abstract  = {Various kinds of typed attributed graphs are used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformations provide a formal model for defining state sequences. We consider the extended case where time elapses between states and introduce a logic to reason about these sequences. With this logic we express properties on the structure and attributes of states as well as on the temporal occurrence of states that are related by their inner structure, which no formal logic over graphs accomplishes concisely so far. Firstly, we introduce graphs with history by equipping every graph element with the timestamp of its creation and, if applicable, its deletion. Secondly, we define a logic on graphs by integrating the temporal operator until into the well-established logic of nested graph conditions. Thirdly, we prove that our logic is equally expressive to nested graph conditions by providing a suitable reduction. Finally, the implementation of this reduction allows for the tool-based analysis of metric temporal properties for state sequences.},
  language  = {en}
}
@book{SchneiderLambersOrejas2017,
  author    = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
  title     = {Symbolic model generation for graph properties},
  number    = {115},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-396-1},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-103171},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {48},
  year      = {2017},
  abstract  = {Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about graph properties. In particular, we want to be able to check automatically if a given graph property is satisfiable. Actually, in most application scenarios it is desirable to be able to explore graphs satisfying the graph property if they exist or even to get a complete and compact overview of the graphs satisfying the graph property. We show that the tableau-based reasoning method for graph properties as introduced by Lambers and Orejas paves the way for a symbolic model generation algorithm for graph properties. Graph properties are formulated in a dedicated logic making use of graphs and graph morphisms, which is equivalent to firstorder logic on graphs as introduced by Courcelle. Our parallelizable algorithm gradually generates a finite set of so-called symbolic models, where each symbolic model describes a set of finite graphs (i.e., finite models) satisfying the graph property. The set of symbolic models jointly describes all finite models for the graph property (complete) and does not describe any finite graph violating the graph property (sound). Moreover, no symbolic model is already covered by another one (compact). Finally, the algorithm is able to generate from each symbolic model a minimal finite model immediately and allows for an exploration of further finite models. The algorithm is implemented in the new tool AutoGraph.},
  language  = {en}
}
@book{BeyhlBlouinGieseetal.2016,
  author    = {Beyhl, Thomas and Blouin, Dominique and Giese, Holger and Lambers, Leen},
  title     = {On the operationalization of graph queries with generalized discrimination networks},
  number    = {106},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-372-5},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-96279},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {33},
  year      = {2016},
  abstract  = {Graph queries have lately gained increased interest due to application areas such as social networks, biological networks, or model queries. For the relational database case the relational algebra and generalized discrimination networks have been studied to find appropriate decompositions into subqueries and ordering of these subqueries for query evaluation or incremental updates of query results. For graph database queries however there is no formal underpinning yet that allows us to find such suitable operationalizations. Consequently, we suggest a simple operational concept for the decomposition of arbitrary complex queries into simpler subqueries and the ordering of these subqueries in form of generalized discrimination networks for graph queries inspired by the relational case. The approach employs graph transformation rules for the nodes of the network and thus we can employ the underlying theory. We further show that the proposed generalized discrimination networks have the same expressive power as nested graph conditions.},
  language  = {en}
}