[isabelle] New in the AFP: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New in the AFP: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
- From: Thiemann, René <Rene.Thiemann at uibk.ac.at>
- Date: Fri, 5 Jul 2019 07:57:11 +0000
- Accept-language: de-DE, de-AT, en-US
- Thread-index: AQHVMwdAXHM8FLfOFkqrlfygMx8fcQ==
- Thread-topic: New in the AFP: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
the AFP has a new entry:
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
by Joshua Schneider and Dmitriy Traytel
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 forthcoming 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and