### 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
temporal logic (MFOTL), an expressive extension of linear temporal
logic with real-time constraints and first-order quantification. The
verified monitor implements a simplified variant of the algorithm used
in the efficient MonPoly monitoring tool. The formalization is
presented in a RV
2019 paper, which also compares the output of the verified
monitor to that of other monitoring tools on randomly generated
inputs. This case study revealed several errors in the optimized but
unverified tools.

### License

### History

- August 13, 2020
- added the formalization of the abstract slicing framework and joint data
slicer (revision b1639ed541b7)

### Topics

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