Standard
Explainable Online Monitoring of Metric Temporal Logic. / Lima, Leonardo; Herasimau, Andrei; Raszyk, Martin; Traytel, Dmitriy; Yuan, Simon.
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings. red. / Sriram Sankaranarayanan; Natasha Sharygina. Springer, 2023. s. 473-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 13994 LNCS).
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
Lima, L, Herasimau, A, Raszyk, M
, Traytel, D & Yuan, S 2023,
Explainable Online Monitoring of Metric Temporal Logic. i S Sankaranarayanan & N Sharygina (red),
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 13994 LNCS, s. 473-491, 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, Frankrig,
22/04/2023.
https://doi.org/10.1007/978-3-031-30820-8_28
APA
Lima, L., Herasimau, A., Raszyk, M.
, Traytel, D., & Yuan, S. (2023).
Explainable Online Monitoring of Metric Temporal Logic. I S. Sankaranarayanan, & N. Sharygina (red.),
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings (s. 473-491). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 13994 LNCS
https://doi.org/10.1007/978-3-031-30820-8_28
Vancouver
Lima L, Herasimau A, Raszyk M
, Traytel D, Yuan S.
Explainable Online Monitoring of Metric Temporal Logic. I Sankaranarayanan S, Sharygina N, red., Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings. Springer. 2023. s. 473-491. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 13994 LNCS).
https://doi.org/10.1007/978-3-031-30820-8_28
Author
Lima, Leonardo ; Herasimau, Andrei ; Raszyk, Martin ; Traytel, Dmitriy ; Yuan, Simon. / Explainable Online Monitoring of Metric Temporal Logic. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings. red. / Sriram Sankaranarayanan ; Natasha Sharygina. Springer, 2023. s. 473-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 13994 LNCS).
Bibtex
@inproceedings{733750649f4547489a489a0eb0194db1,
title = "Explainable Online Monitoring of Metric Temporal Logic",
abstract = "Runtime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor{\textquoteright}s user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.",
keywords = "certification, explanations, formal verification, metric temporal logic, proof system, runtime monitoring",
author = "Leonardo Lima and Andrei Herasimau and Martin Raszyk and Dmitriy Traytel and Simon Yuan",
note = "Publisher Copyright: {\textcopyright} 2023, The Author(s).; 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023 ; Conference date: 22-04-2023 Through 27-04-2023",
year = "2023",
doi = "10.1007/978-3-031-30820-8_28",
language = "English",
isbn = "9783031308192",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "473--491",
editor = "Sriram Sankaranarayanan and Natasha Sharygina",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings",
address = "Switzerland",
}
RIS
TY - GEN
T1 - Explainable Online Monitoring of Metric Temporal Logic
AU - Lima, Leonardo
AU - Herasimau, Andrei
AU - Raszyk, Martin
AU - Traytel, Dmitriy
AU - Yuan, Simon
N1 - Publisher Copyright:
© 2023, The Author(s).
PY - 2023
Y1 - 2023
N2 - Runtime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor’s user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.
AB - Runtime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor’s user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.
KW - certification
KW - explanations
KW - formal verification
KW - metric temporal logic
KW - proof system
KW - runtime monitoring
UR - http://www.scopus.com/inward/record.url?scp=85161470218&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-30820-8_28
DO - 10.1007/978-3-031-30820-8_28
M3 - Article in proceedings
AN - SCOPUS:85161470218
SN - 9783031308192
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 473
EP - 491
BT - Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings
A2 - Sankaranarayanan, Sriram
A2 - Sharygina, Natasha
PB - Springer
T2 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023
Y2 - 22 April 2023 through 27 April 2023
ER -
