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

BSD 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

### Session MFOTL_Monitor

- Trace
- Table
- Abstract_Monitor
- Interval
- MFOTL
- Monitor
- Slicing
- Monitor_Code
- Examples

### Depends on

- Light-weight Containers

### Used by

- A Verified Proof Checker for Metric First-Order Temporal Logic
- Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
- Formalization of Multiway-Join Algorithms

### Auto-related entries

- Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
- A Verified Proof Checker for Metric First-Order Temporal Logic
- A Compositional and Unified Translation of LTL into ω-Automata
- Linear Temporal Logic
- Formalization of Refinement Calculus for Reactive Systems

## Cite

×

MFOTL_Monitor-AFP

    @article{MFOTL_Monitor-AFP,
      author  = {Joshua Schneider and Dmitriy Traytel},
      title   = {Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/MFOTL_Monitor.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jul 5, 2019 : Isabelle2019