• search hit 3 of 3
Back to Result List

Metric temporal graph logic over typed attributed graphs

  • 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 allowsVarious 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.show moreshow less
  • 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 denVerschiedene 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.show moreshow less

Download full text files

  • tbhpi123.pdfeng
    (1802KB)

    SHA-1:9fba63f220d5bfd133fad025daa8da1ca2f005b6

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Holger GieseORCiDGND, Maria Maximova, Lucas Sakizloglou, Sven Schneider
URN:urn:nbn:de:kobv:517-opus4-411351
ISBN:978-3-86956-433-3
ISSN:1613-5652
ISSN:2191-1665
Series (Serial Number):Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (123)
Publisher:Universitätsverlag Potsdam
Place of publication:Potsdam
Document Type:Monograph/Edited Volume
Language:English
Year of Completion:2018
Publishing Institution:Universität Potsdam
Publishing Institution:Universitätsverlag Potsdam
Release Date:2018/10/22
Tag:Runtime-monitoring; Sequenzeigenschaften; Temporallogik; getypte Attributierte Graphen; metrische Temporallogik; symbolische Graphen; verschachtelte Anwendungsbedingungen
metric temporal logic; nested graph conditions; runtime monitoring; sequence properties; symbolic graphs; temporal logic; typed attributed graphs
Issue:123
Pagenumber:29
RVK - Regensburg Classification:ST 230
Organizational units:Digital Engineering Fakultät / Hasso-Plattner-Institut für Digital Engineering GmbH
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Publication Way:Universitätsverlag Potsdam
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Notes extern:
In Printform erschienen im Universitätsverlag Potsdam:

Metric Temporal Graph Logic over Typed Attributed Graphs / Holger Giese, Maria Maximova, Lucas Sakizloglou, Sven Schneider. – Potsdam: Universitätsverlag Potsdam, 2018. – 29 S.
(Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam ; 123)
ISSN (print) 1613-5652
ISSN (online) 2191-1665
ISBN 978-3-86956-433-3
--> bestellen