Standard
Explainable Online Monitoring of Metric First-Order Temporal Logic. / Lima, Leonardo; Huerta y Munive, Jonathan Julián; Traytel, Dmitriy.
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings. red. / Bernd Finkbeiner; Laura Kovács. Springer, 2024. s. 288-307 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 14570 LNCS).
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
Lima, L, Huerta y Munive, JJ
& Traytel, D 2024,
Explainable Online Monitoring of Metric First-Order Temporal Logic. i B Finkbeiner & L Kovács (red),
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 14570 LNCS, s. 288-307, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxemborg,
06/04/2024.
https://doi.org/10.1007/978-3-031-57246-3_16
APA
Lima, L., Huerta y Munive, J. J.
, & Traytel, D. (2024).
Explainable Online Monitoring of Metric First-Order Temporal Logic. I B. Finkbeiner, & L. Kovács (red.),
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings (s. 288-307). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 14570 LNCS
https://doi.org/10.1007/978-3-031-57246-3_16
Vancouver
Lima L, Huerta y Munive JJ
, Traytel D.
Explainable Online Monitoring of Metric First-Order Temporal Logic. I Finkbeiner B, Kovács L, red., Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings. Springer. 2024. s. 288-307. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 14570 LNCS).
https://doi.org/10.1007/978-3-031-57246-3_16
Author
Lima, Leonardo ; Huerta y Munive, Jonathan Julián ; Traytel, Dmitriy. / Explainable Online Monitoring of Metric First-Order Temporal Logic. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings. red. / Bernd Finkbeiner ; Laura Kovács. Springer, 2024. s. 288-307 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 14570 LNCS).
Bibtex
@inproceedings{6bc14535b25b4378b1fabca2c8214824,
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 {Huerta y Munive}, {Jonathan Juli{\'a}n} and Dmitriy Traytel",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.; 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 ; Conference date: 06-04-2024 Through 11-04-2024",
year = "2024",
doi = "10.1007/978-3-031-57246-3_16",
language = "English",
isbn = "9783031572456",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "288--307",
editor = "Bernd Finkbeiner and Laura Kov{\'a}cs",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings",
address = "Switzerland",
}
RIS
TY - GEN
T1 - Explainable Online Monitoring of Metric First-Order Temporal Logic
AU - Lima, Leonardo
AU - Huerta y Munive, Jonathan Julián
AU - Traytel, Dmitriy
N1 - Publisher Copyright:
© The Author(s) 2024.
PY - 2024
Y1 - 2024
N2 - 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’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.
AB - 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’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.
U2 - 10.1007/978-3-031-57246-3_16
DO - 10.1007/978-3-031-57246-3_16
M3 - Article in proceedings
AN - SCOPUS:85192166399
SN - 9783031572456
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 288
EP - 307
BT - Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings
A2 - Finkbeiner, Bernd
A2 - Kovács, Laura
PB - Springer
T2 - 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
Y2 - 6 April 2024 through 11 April 2024
ER -
