|
Multi-Head
Monitoring
of
Metric
Dynamic
Logic
Title: |
Multi-Head Monitoring of Metric Dynamic Logic |
Author:
|
Martin Raszyk (martin /dot/ raszyk /at/ inf /dot/ ethz /dot/ ch)
|
Submission date: |
2022-02-13 |
Abstract: |
Runtime monitoring (or runtime verification) is an approach to
checking compliance of a system's execution with a specification
(e.g., a temporal query). The system's execution is logged into a
trace---a sequence of time-points, each consisting of a time-stamp and
observed events. A monitor is an algorithm that produces verdicts on
the satisfaction of a temporal query on a trace. We formalize a
monitoring algorithm for metric dynamic logic, an extension of metric
temporal logic with regular expressions. The monitor computes whether
a given query is satisfied at every position in an input trace of
time-stamped events. We formalize the time-stamps as an abstract
algebraic structure satisfying certain assumptions. Instances of this
structure include natural numbers, real numbers, and lexicographic
combinations of them. Our monitor follows the multi-head paradigm: it
reads the input simultaneously at multiple positions and moves its
reading heads asynchronously. This mode of operation results in
unprecedented time and space complexity guarantees for metric dynamic
logic: The monitor's amortized time complexity to process a
time-point and the monitor's space complexity neither depends on
the event-rate, i.e., the number of events within a fixed time-unit,
nor on the numeric constants occurring in the quantitative temporal
constraints in the given query. The multi-head monitoring algorithm
for metric dynamic logic is reported in our paper "Multi-Head
Monitoring of Metric Dynamic Logic" published at ATVA 2020. We
have also formalized unpublished specialized algorithms for the
temporal operators of metric temporal logic. |
BibTeX: |
@article{VYDRA_MDL-AFP,
author = {Martin Raszyk},
title = {Multi-Head Monitoring of Metric Dynamic Logic},
journal = {Archive of Formal Proofs},
month = feb,
year = 2022,
note = {\url{https://isa-afp.org/entries/VYDRA_MDL.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Containers |
|