DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2008.1740

Runtime Monitoring of Metric First-order Temporal Properties

Authors: David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract

We introduce a novel approach to the runtime monitoring of complex system properties. In particular, we present an online algorithm for a safety fragment of metric first-order temporal logic that is considerably more expressive than the logics supported by prior monitoring methods. Our approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinite domains, and the arbitrary nesting of both past and bounded future operators. Moreover, we show how to optimize our approach for the common case where structures consist of only finite relations, over possibly infinite domains. Under an additional restriction, we prove that the space consumed by our monitor is polynomially bounded by the cardinality of the data appearing in the processed prefix of the temporal structure being monitored.

Cite as

David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann. Runtime Monitoring of Metric First-order Temporal Properties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{basin_et_al:LIPIcs.FSTTCS.2008.1740,
  author =	{Basin, David and Klaedtke, Felix and M\"{u}ller, Samuel and Pfitzmann, Birgit},
  title =	{{Runtime Monitoring of Metric First-order Temporal Properties}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{49--60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1740},
  URN =		{urn:nbn:de:0030-drops-17404},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1740},
  annote =	{Keywords: Runtime Monitoring, Metric First-order Temporal Logic, Automatic Structures, Temporal Databases}
}

Search Results

Documents authored by Müller, Samuel

Runtime Monitoring of Metric First-order Temporal Properties

Abstract

Cite as

Thanks for your feedback!

Could not send message