Reference:
, "Metric Temporal Graph Logic over Typed Attributed Graphs", in Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic April 6-11, 2019, Proceedings, pp. 282–298, 2019.
Abstract:
Various kinds of typed attributed graphs can be used to rep- resent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformation can provide a formal model for defining state sequences. We consider the case where time may elapse between state changes and introduce a logic, called Metric Temporal Graph Logic (MTGL), to reason about such timed graph sequences. With this logic, we express properties on the structure and attributes of states as well as on the occurrence of states over time that are related by their inner structure, which no formal logic over graphs concisely accomplishes so far. Firstly, based on timed graph sequences as models for system evolution, we define MTGL by integrating the temporal operator until with time bounds into the well-established logic of (nested) graph conditions. Secondly, we outline how a finite timed graph sequence can be represented as a single graph containing all changes over time (called graph with history), how the satisfaction of MTGL conditions can be defined for such a graph and show that both representations satisfy the same MTGL conditions. Thirdly, we present how MTGL conditions can be reduced to (nested) graph conditions and show using this reduction that both underlying logics are equally expressive. Finally, we present an extension of the tool AutoGraph allowing to check the satisfaction of MTGL conditions for timed graph sequences, by checking the satisfaction of the (nested) graph conditions, obtained using the proposed reduction, for the graph with history corresponding to the timed graph sequence.
Links:
@InProceedings{DBLP:conffaseGieseMSS19_1,
AUTHOR = {Giese, Holger and Maximova, Maria and Sakizloglou, Lucas and Schneider, Sven},
TITLE = {{Metric Temporal Graph Logic over Typed Attributed Graphs}},
YEAR = {2019},
BOOKTITLE = {Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic April 6-11, 2019, Proceedings},
PAGES = {282--298},
CROSSREF = {DBLP:conf/fase/2019},
URL = {doi.org/10.1007/978-3-030-16722-6_16},
PDF = {uploads/pdf/DBLP:conffaseGieseMSS19_1_main.pdf},
OPTacc_pdf = {},
ABSTRACT = {Various kinds of typed attributed graphs can be used to rep-
resent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformation can provide a formal model for defining state sequences. We consider the case where time may elapse between state changes and introduce a logic, called Metric Temporal Graph Logic (MTGL), to reason about such timed graph sequences. With this logic, we express properties on the structure and attributes of states as well as on the occurrence of states over time that are related by their inner structure, which no formal logic over graphs concisely accomplishes so far.
Firstly, based on timed graph sequences as models for system evolution, we define MTGL by integrating the temporal operator until with time bounds into the well-established logic of (nested) graph conditions. Secondly, we outline how a finite timed graph sequence can be represented as a single graph containing all changes over time (called graph with history), how the satisfaction of MTGL conditions can be defined for such a graph and show that both representations satisfy the same MTGL conditions. Thirdly, we present how MTGL conditions can be reduced to (nested) graph conditions and show using this reduction that both underlying logics are equally expressive. Finally, we present an extension
of the tool AutoGraph allowing to check the satisfaction of MTGL conditions for timed graph sequences, by checking the satisfaction of the (nested) graph conditions, obtained using the proposed reduction, for the graph with history corresponding to the timed graph sequence.},
ANNOTE = {TIMESTAMP : Thu, 04 Apr 2019 12:18:13 +0200}
}