License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2008.1740
URN: urn:nbn:de:0030-drops-17404
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1740/
Go to the corresponding LIPIcs Volume Portal

Basin, David ; Klaedtke, Felix ; Müller, Samuel ; Pfitzmann, Birgit

Runtime Monitoring of Metric First-order Temporal Properties

pdf-format:
08004.BasinDavid.1740.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{basin_et_al:LIPIcs:2008:1740,
  author =	{David Basin and Felix Klaedtke and Samuel M{\"u}ller and Birgit Pfitzmann},
  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 =	{Ramesh Hariharan and Madhavan Mukund and V Vinay},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/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}
}

Keywords: Runtime Monitoring, Metric First-order Temporal Logic, Automatic Structures, Temporal Databases
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue Date: 2008
Date of publication: 05.12.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI