| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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{https://isa-afp.org/entries/MFODL_Monitor_Optimized.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Generic_Join, IEEE_Floating_Point, MFOTL_Monitor |
| 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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |