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

### License

### History

- October 19, 2021
- corrected a mistake in the calculation of median aggregations
(reported by Nicolas Kaletsch, revision 02b14c9bf3da)

### Topics

- Computer science/Algorithms
- Logic/General logic/Modal logic
- Computer science/Automata and formal languages