Runtime Monitoring of Metric First-order Temporal Properties

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

doi:10.4230/LIPIcs.FSTTCS.2008.1740

Document

Runtime Monitoring of Metric First-order Temporal Properties

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

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2008-12-05

PDF

File

PDF

LIPIcs.FSTTCS.2008.1740.pdf

Filesize: 439 kB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2008.1740
URN: urn:nbn:de:0030-drops-17404

Subject Classification

Keywords

Runtime Monitoring
Metric First-order Temporal Logic
Automatic Structures
Temporal Databases

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1740

Author Details

David Basin

Felix Klaedtke

Samuel Müller

Birgit Pfitzmann

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail