Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic (Q7361410)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry MFOTL_Monitor
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic |
AFP entry MFOTL_Monitor |
Statements
4 July 2019
0 references
Joshua Schneider
0 references
Dmitriy Traytel
0 references
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic (English)
0 references
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.
0 references
