Explainable Online Monitoring of Metric Temporal Logic
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- Fulltext
Final published version, 942 KB, PDF document
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.
Original language | English |
---|---|
Title of host publication | 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 |
Editors | Sriram Sankaranarayanan, Natasha Sharygina |
Publisher | Springer |
Publication date | 2023 |
Pages | 473-491 |
ISBN (Print) | 9783031308192 |
DOIs | |
Publication status | Published - 2023 |
Event | 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, France Duration: 22 Apr 2023 → 27 Apr 2023 |
Conference
Conference | 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 | France |
By | Paris |
Periode | 22/04/2023 → 27/04/2023 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 13994 LNCS |
ISSN | 0302-9743 |
Bibliographical note
Publisher Copyright:
© 2023, The Author(s).
- certification, explanations, formal verification, metric temporal logic, proof system, runtime monitoring
Research areas
Number of downloads are based on statistics from Google Scholar and www.ku.dk
ID: 357279437