### Abstract

Runtime monitoring (or runtime verification) is an approach to checking compliance of a system's execution with a specification (e.g., a temporal formula). 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 formula on a trace.

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. We also include the formalization of a conversion from the abstract time domain introduced by Koymans (1990) to our time-stamps.

We formalize a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given formula is satisfied at every position in an input trace of time-stamped events. 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 formula.

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.

### License

BSD License

### History

February 23, 2022
  added conversion from the abstract time domain by Koymans (1990) to our time domain; refactored assumptions on time domain (revision c9f94b0ae10e)

### Topics

- Computer science/Algorithms

### Session VYDRA_MDL

- Timestamp
- Interval
- Trace
- MDL
- Metric_Point_Structure
- NFA
- Window
- Temporal
- Monitor
- Preliminaries
- Monitor_Code
- Timestamp_Lex
- Timestamp_Prod

### Depends on

- Light-weight Containers

### Auto-related entries

- Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

## Cite

×

VYDRA_MDL-AFP

    @article{VYDRA_MDL-AFP,
      author  = {Martin Raszyk},
      title   = {Multi-Head Monitoring of Metric Dynamic Logic},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/VYDRA_MDL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 14, 2022 : Isabelle2021-1