TY - BOOK A1 - Giese, Holger A1 - Maximova, Maria A1 - Sakizloglou, Lucas A1 - Schneider, Sven T1 - Metric temporal graph logic over typed attributed graphs N2 - 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. N2 - Verschiedene Arten von getypten attributierten Graphen werden benutzt, um Zustände von Systemen in vielen unterschiedlichen Anwendungsbereichen zu beschreiben. Der etablierte Formalismus der Graphtransformationen bietet ein formales Model, um Zustandssequenzen für dynamische Systeme zu definieren. Wir betrachten den erweiterten Fall von solchen Sequenzen, in dem Zeit zwischen zwei verschiedenen Systemzuständen vergeht, und führen eine Logik ein, um solche Sequenzen zu beschreiben. Mit dieser Logik drücken wir zum einen Eigenschaften über die Struktur und die Attribute von Zuständen aus und beschreiben zum anderen temporale Vorkommen von Zuständen, die durch ihre innere Struktur verbunden sind. Solche Eigenschaften können bisher von keiner der existierenden Logiken auf Graphen vergleichbar darstellt werden. Erstens führen wir Graphen mit Änderungshistorie ein, indem wir jedes Graphelement mit einem Zeitstempel seiner Erzeugung und, wenn nötig, seiner Löschung versehen. Zweitens definieren wir eine Logik auf Graphen, indem wir den Temporaloperator Until in die wohl-etablierte Logik der verschachtelten Graphbedingungen integrieren. Drittens beweisen wir, dass unsere Logik gleich ausdrucksmächtig ist, wie die Logik der verschachtelten Graphbedingungen, indem wir eine passende Reduktionsoperation definieren. Zuletzt erlaubt uns die Implementierung dieser Reduktionsoperation die werkzeukbasierte Analyse von metrisch-temporallogischen Eigenschaften für Zustandssequenzen zu führen. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 123 KW - nested graph conditions KW - sequence properties KW - symbolic graphs KW - typed attributed graphs KW - metric temporal logic KW - temporal logic KW - runtime monitoring KW - verschachtelte Anwendungsbedingungen KW - Sequenzeigenschaften KW - symbolische Graphen KW - getypte Attributierte Graphen KW - metrische Temporallogik KW - Temporallogik KW - Runtime-monitoring Y1 - 2018 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-411351 SN - 978-3-86956-433-3 SN - 1613-5652 SN - 2191-1665 IS - 123 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - A logic-based incremental approach to graph repair T1 - Ein logikbasierter inkrementeller Ansatz für Graphreparatur N2 - 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. N2 - Die Reparatur von Graphen, die Wiederherstellung der Konsistenz eines Graphen, spielt in mehreren Bereichen der Informatik und darüber hinaus eine herausragende Rolle: Beispielsweise wird in der modellgetriebenen Konstruktion die abstrakte Syntax von Modellen in der Regel mithilfe von Graphen kodiert. Flexible Bearbeitungsvorgänge erstellen vorübergehend inkonsistente Diagramme, die kein gültiges Modell darstellen, und erfordern daher eine Reparatur des Diagramms. Auf ähnliche Weise können Aktualisierungen in Graphendatenbanken - die das Speichern und Bearbeiten von Graphendaten verwalten - dazu führen, dass eine bestimmte Datenbank einige Integritätsbeschränkungen nicht erfüllt und auch eine Graphreparatur erforderlich macht. Wir präsentieren einen logikbasierten inkrementellen Ansatz für die Graphreparatur, der eine solide und vollständige (nach Beendigung) Übersicht über die am wenigsten verändernden Reparaturen erstellt. In unserem Kontext formalisieren wir die Konsistenz mittels sogenannten Graphbedingungen die der Logik erster Ordnung in Graphen entsprechen. Wir stellen zwei Arten von Reparaturalgorithmen vor: Die zustandsbasierte Reparatur stellt die Konsistenz unabhängig vom Verlauf der Graphänderung wieder her, während die deltabasierte (oder inkrementelle) Reparatur diesen Verlauf explizit berücksichtigt. Technisch stützen sich unsere Algorithmen auf einen vorhandenen Modellgenerierungsalgorithmus für in AutoGraph implementierte Graphbedingungen. Darüber hinaus verwendet der deltabasierte Ansatz das neue Konzept der Erfüllungsbäume (STs) zum Kodieren, ob und wie ein Graph eine Graphbedingung erfüllt. Wir zeigen dann, wie diese STs in Bezug auf eine Graphaktualisierung inkrementell manipuliert werden. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 126 KW - nested graph conditions KW - graph repair KW - model repair KW - consistency restoration KW - verschachtelte Graphbedingungen KW - Graphreparatur KW - Modellreparatur KW - Konsistenzrestauration Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-427517 SN - 978-3-86956-462-3 SN - 1613-5652 SN - 2191-1665 IS - 126 PB - Universitätsverlag Potsdam CY - Potsdam ER -