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

Thibault Dardinier, Lukas Heimes, Martin Raszyk 📧, Joshua Schneider 📧 and Dmitriy Traytel 🌐

April 9, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.
BSD License

Change history

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

Topics

Theories of MFODL_Monitor_Optimized