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