@inbook{76cc84b1846d49689b1e005105dcfa0a,
title = "Explainable Online Monitoring of Metric First-Order Temporal Logic",
abstract = "Metric first-order temporal logic (MFOTL) is an expressive formalism for specifying temporal and data-dependent constraints on streams of time-stamped, data-carrying events. It serves as the specification language of several runtime monitors. These monitors input an MFOTL formula and an event stream prefix and output satisfying assignments to the formula{\textquoteright}s free variables. For complex formulas, it may be unclear why a certain assignment is output. We propose an approach that accompanies assignments with detailed explanations, in the form of proof trees. We develop a new monitor that outputs such explanations. Our tool incorporates a formally verified checker that certifies the explanations and a visualization that allows users to interactively explore and understand the outputs.",
author = "Leonardo Lima and Munive, {Jonathan Juli{\'a}n Huerta y} and Dmitriy Traytel",
year = "2024",
doi = "10.1007/978-3-031-57246-3_16",
language = "English",
isbn = "9783031572456",
series = "Lecture Notes in Computer Science",
publisher = "Physica-Verlag",
pages = "288--307",
editor = "Bernd Finkbeiner and Laura Kov{\'a}cs",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
}