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

 Title: Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations Authors: Thibault Dardinier, Lukas Heimes, Martin Raszyk (martin /dot/ raszyk /at/ inf /dot/ ethz /dot/ ch), Joshua Schneider and Dmitriy Traytel Submission date: 2020-04-09 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. BibTeX: @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 = apr, year = 2020, note = {\url{http://isa-afp.org/entries/MFODL_Monitor_Optimized.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Containers, Generic_Join, IEEE_Floating_Point Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.