From LTL to rLTL monitoring: improved monitorability through robust semantics

DOI10.1007/s10703-022-00398-4zbMath1522.68334OpenAlexW2945603833MaRDI QIDQ6108436

Daniel Neider, Maximilian Schwenger, Martin Zimmermann, Corto N. Mascle, Alexander Weinert, Paulo Tabuada

Publication date: 29 June 2023

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-022-00398-4

zbMATH Keywords

runtime monitoringrobust linear temporal logic

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Robustness of temporal logic specifications for continuous-time signals
• Collecting statistics over runtime executions
• Monitoring of temporal first-order properties with aggregations
• Quantitative monitoring of STL with edit distance
• Time robustness in MTL and expressivity in hybrid system falsification
• The complexity of counting models of linear-time temporal logic
• Automated technology for verification and analysis. 16th international symposium, ATVA 2018, Los Angeles, CA, USA, October 7--10, 2018. Proceedings
• An overview of the runtime verification tool Java PathExplorer
• Robust, expressive, and quantitative linear temporal logics: pick any two for free
• Regular Programming for Quantitative Properties of Data Streams
• Temporal Logic as Filtering
• Comparing LTL Semantics for Runtime Verification
• Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors
• Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic
• The Density of Linear-Time Properties
• From LTL to rLTL monitoring
• Quantitative Regular Expressions for Arrhythmia Detection Algorithms
• Evrostos
• Robust Linear Temporal Logic
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Model checking of safety properties
• A counting semantics for monitoring LTL specifications over finite traces
• Signal convolution logic
• Owl: a library for \(\omega \)-words, automata, and LTL

This page was built for publication: From LTL to rLTL monitoring: improved monitorability through robust semantics