Email Gateway (Aug 23 2022 at 08:53): Email Gateway (Aug 23 2022 at 08:53):From: Tobias Nipkow <nipkow@in.tum.de>
Formalization of an Optimized Monitoring Algorithm for Metric First-Order
Dynamic Logic with Aggregations
Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
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.
https://www.isa-afp.org/entries/MFODL_Monitor_Optimized.html
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 12:28 UTC