### Abstract

A monitor is a runtime verification tool that solves the following problem: Given a stream of time-stamped events and a policy formulated in a specification language, decide whether the policy is satisfied at every point in the stream. We verify the correctness of an executable monitor for specifications given as formulas in metric first-order dynamic logic (MFODL), which combines the features of metric first-order temporal logic (MFOTL) and metric dynamic logic. Thus, MFODL supports real-time constraints, first-order parameters, and regular expressions. Additionally, the monitor supports aggregation operations such as count and sum. This formalization, which is described in a forthcoming paper at IJCAR 2020, significantly extends previous work on a verified monitor for MFOTL. Apart from the addition of regular expressions and aggregations, we implemented multi-way joins and a specialized sliding window algorithm to further optimize the monitor.

### License

BSD License

### History

October 19, 2021
  corrected a mistake in the calculation of median aggregations (reported by Nicolas Kaletsch, revision 02b14c9bf3da)

### Topics

- Computer science/Algorithms
- Logic/General logic/Modal logic
- Computer science/Automata and formal languages

### Session MFODL_Monitor_Optimized

- Code_Double
- Event_Data
- Regex
- Formula
- Optimized_Join
- Monitor
- Optimized_MTL
- Monitor_Impl
- Monitor_Code

### Depends on

- Formalization of Multiway-Join Algorithms
- A Formal Model of IEEE Floating Point Arithmetic
- Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

### Auto-related entries

- Multi-Head Monitoring of Metric Dynamic Logic
- A Verified Proof Checker for Metric First-Order Temporal Logic

## Cite

×

MFODL_Monitor_Optimized-AFP

    @article{MFODL_Monitor_Optimized-AFP,
      author  = {Thibault Dardinier and Lukas Heimes and Martin Raszyk and Joshua Schneider and Dmitriy Traytel},
      title   = {Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/MFODL_Monitor_Optimized.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Apr 12, 2020 : Isabelle2019
- Apr 11, 2020 : Isabelle2019