Explainable online monitoring of metric temporal logic

DOI10.1007/978-3-031-30820-8_28MaRDI QIDQ6536149zbMATH OpenFDO

Authors L. S. Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan

Publication date 5 April 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

metric temporal logicformal verificationcertificationproof systemruntime monitoringexplanations

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Computer says no: verdict explainability for runtime monitors using a local proof system
• On monitoring linear temporal properties
• Multi-head monitoring of metric temporal logic
• Monitoring metric first-order temporal properties
• Runtime monitoring of metric first-order temporal properties

Cites work

• Algorithms for monitoring real-time properties
• Almost event-rate independent monitoring
• Certifying emptiness of timed Büchi automata
• Computer says no: verdict explainability for runtime monitors using a local proof system
• Constructive finite trace analysis with linear temporal logic
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Fundamental Approaches to Software Engineering
• Localizing Faults in Simulink/Stateflow Models with STL
• Monitoring metric first-order temporal properties
• Multi-head Monitoring of Metric Dynamic Logic
• Multi-head monitoring of metric temporal logic
• Optimal proofs for linear temporal logic on lasso words
• POSIX regular expression parsing with derivatives
• Verified certification of reachability checking for timed automata

This page was built for publication: Explainable online monitoring of metric temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536149)