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