Explainable Online Monitoring of Metric Temporal Logic

Leonardo Lima; Andrei Herasimau; Martin Raszyk; Dmitriy Traytel; Simon Yuan

doi:10.1007/978-3-031-30820-8_28

Explainable Online Monitoring of Metric Temporal Logic

Leonardo Lima^*, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan

^*Corresponding author af dette arbejde

Software, Data, People & Society

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

5 Citationer (Scopus)

29 Downloads (Pure)

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’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.

Originalsprog	Engelsk
Titel	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
Redaktører	Sriram Sankaranarayanan, Natasha Sharygina
Forlag	Springer
Publikationsdato	2023
Sider	473-491
ISBN (Trykt)	9783031308192
DOI	https://doi.org/10.1007/978-3-031-30820-8_28
Status	Udgivet - 2023
Begivenhed	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 Varighed: 22 apr. 2023 → 27 apr. 2023

Konference

Konference	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
Land/Område	Frankrig
By	Paris
Periode	22/04/2023 → 27/04/2023

Navn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	13994 LNCS
ISSN	0302-9743

Bibliografisk note

Publisher Copyright:
© 2023, The Author(s).

Adgang til dokumentet

10.1007/978-3-031-30820-8_28Licens: CC BY

FulltextForlagets udgivne version, 942 KBLicens: CC BY

Citationsformater

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

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 › peer review

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

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

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).

@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",

}

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

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 -