Runtime Verification: 24th International Conference, RV 2024, Istanbul, Turkey, October 15–17, 2024, Proceedings

Preface
Organization
Distributed Runtime Verification with Imperfect Monitors: Challenges and Opportunities (Extended Abstract)
Contents
Cyber-physical Systems
A Formal Approach for Safe Reinforcement Learning: A Rate-Adaptive Pacemaker Case Study
	1 Introduction
	2 Overview of the Proposed Approach
	3 Case-Study and Problem Discussion
		3.1 Cardiac Conduction System
		3.2 Pacemakers
		3.3 Setup of the Proposed Approach
	4 Properties as Discrete Timed Automata
	5 Discrete Timed Automaton Based Runtime Enforcement for Safe Reinforcement Learning
	6 Implementation and Scenarios
	7 Results
	8 Related Work
	9 Conclusion
	References
Stream-Based Monitoring Under Measurement Noise
	1 Introduction
		1.1 Motivating Example
		1.2 Related Work
	2 Preliminaries
		2.1 Lola
		2.2 Error Model
	3 Robust Lola
	4 Approximate Online Monitoring
	5 Precise Constant Memory Online Monitoring
	6 Evaluation
	7 Conclusion
	References
Dynamic, Multi-objective Specification and Falsification of Autonomous CPS
	1 Introduction
	2 Formulation of Dynamic Rulebooks
	3 Problem Formulation
	4 Our Framework
		4.1 Overview of Our Framework
		4.2 Our Sampling Algorithm
		4.3 Extension to a Generic Framework
	5 Scenarios
	6 Experiments
		6.1 Results
		6.2 Discussion
	7 Conclusion
	References
Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption
	1 Background
	2 Oblivious Online Discrete-Time STL Monitoring
		2.1 Scheme Switching Optimized with Value Range Information
	3 Experimental Evaluation
		3.1 Benchmarks
		3.2 Experiments
		3.3 RQ1: Performance on Practical Benchmarks
		3.4 RQ2: Acceleration by the Optimized Scheme Switching
		3.5 RQ3: Comparison with Purely TFHE-Based Approach
		3.6 RQ4: Computational Demand of the Client
	4 Related Works
	5 Conclusions and Future Work
	References
Sampling-Based and Gradient-Based Efficient Scenario Generation
	1 Introduction
	2 Preliminaries
		2.1 Problem Definition
	3 Scenario Generation Using Path Planning and Model Checking
	4 Neurosymbolic Scenario Generation
	5 Case Studies
		5.1 An Industrial Factory Floor Environment
		5.2 Autonomous Driving
		5.3 Results
	6 Related Work and Conclusions
	References
HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical Systems
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 Parametric Signal Temporal Logic (pSTL)
		3.2 Gaussian Process Regression
		3.3 Part-X Algorithm
	4 Problem Formulation
	5 HyperPart-X Algorithm
	6 Results and Discussion
	7 Conclusions
	References
Temporal Logics
faRM-LTL: A Domain-Specific Architecture for Flexible and Accelerated Runtime Monitoring of LTL Properties
	1 Introduction
	2 Related Works
		2.1 Hardware Regex Matching Engines
	3 Background and Motivation
		3.1 Syntax and Semantics of LTL
		3.2 Runtime Verification of Properties Specified in LTL
		3.3 Regular Expression Matching
		3.4 Employing a Regular Expression Matcher as a Runtime Verification monitor
	4 faRM-LTL
		4.1 Overview
		4.2 Prefix Generator
		4.3 Prefix Translator
		4.4 Monitor
	5 Experiments
		5.1 Weakly Monitorable Properties
		5.2 Area Overhead
	6 Conclusions
	References
Efficient Offline Monitoring for Dynamic Metric Temporal Logic
	1 Introduction
	2 Dynamic Metric Temporal Logic
	3 Efficient Monitoring
		3.1 Monitor for the Formula p \"426830A r[0,)
		3.2 Monitor for the Formula p \"426830A r[a,) Where a 1
		3.3 Monitor for the Formula p \"426830A r[0,b]
		3.4 Monitor for the Formula p \"426830A r[a,b]
		3.5 Overall Monitoring Algorithm
	4 Related Work
	5 Conclusion
	References
TimelyMon: A Streaming Parallel First-Order Monitor
	1 Introduction
	2 Preliminaries
	3 Monitoring Algorithm Overview
	4 Empirical Evaluation
		4.1 Experimental Setup
		4.2 Data and Analysis
	References
Specification and Visualization
Adding State to Stream Runtime Verification
	1 Introduction
	2 States in TeSSLa Yesterday
	3 States in TeSSLa Today
	4 Implementation
	5 Conclusions and Future Work
	References
The Complexity of Data-Free Nfer
	1 Introduction
	2 Data-Free Nfer
	3 Satisfiability
		3.1 Data-Free nfer Satisfiability is Undecidable
		3.2 Inclusive Data-Free nfer Satisfiability is in PTime
		3.3 Cycle-Free Data-Free nfer Satisfiability is Decidable
	4 Evaluation of Data-Free nfer
	5 Conclusion and Future Work
	References
RTLolaMo3Vis - A Mobile and Modular Visualization Framework for Online Monitoring
	1 Introduction
		1.1 Related Work
	2 RTLola
	3 Framework
	4 Implementation and Experiments
		4.1 Technical Setup
		4.2 Visualization Pipeline
	5 Evaluation
	6 Conclusion
	References
Deep Neural Networks
Case Study: Runtime Safety Verification of Neural Network Controlled System
	1 Introduction
	2 Related Work
	3 POLAR-Express Case Study
		3.1 Preliminary
		3.2 Task Specification
		3.3 Runtime Verification (POLAR-Express) Based Safe Control
	4 Experiments
	5 Conclusion and Future Work
	A  Turtlebot Specification
	References
Gaussian-Based and Outside-the-Box Runtime Monitoring Join Forces
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 Neural Networks
		3.2 Monitors
		3.3 Neuron Selection via Gradient Analysis
	4 Methodology
		4.1 Combining Gaussian Monitor and Box Monitor
		4.2 Neuron Selection for Monitoring
	5 Evaluation
		5.1 Experimental Setup and Implementation
		5.2 Results
		5.3 Discussion
	6 Conclusion and Future Work
	References
Box-Based Monitor Approach for Out-of-Distribution Detection in YOLO: An Exploratory Study
	1 Introduction
	2 Problem Statement
	3 Approach
		3.1 Basic Notions
		3.2 Monitor Construction
		3.3 Monitor Deployment
	4 Experiments
		4.1 Experiment Setup
		4.2 Results
	5 Related and Future Work
	6 Conclusion
	References
Distributed Systems
Distributed Monitoring of Timed Properties
	1 Introduction
	2 Preliminaries
		2.1 Distributed Timed Systems
		2.2 Timed Words and Languages
		2.3 Approximate Timed Words
		2.4 Formalism for Timed Systems
	3 Monitoring with Complete Information
		3.1 Point of Certainty
		3.2 Verdicts at tmin 1 -
		3.3 Data Structure
		3.4 Monitoring at tmin 1(.) -
	4 Conclusion
	References
Towards Efficient Runtime Verified Linearizable Algorithms
	1 Introduction
	2 Preliminaries
	3 An Interactive Model for Runtime Verification
	4 The Wrapper A+
	5 From Views to Tight Executions
	6 The Verifier V+
	7 The Lightweight Runtime Verified B+
	8 Conclusions
	References
Approximate Distributed Monitoring Under Partial Synchrony: Balancing Speed & Accuracy
	1 Introduction
	2 Preliminaries
	3 Overapproximation of the STL Distributed Semantics
	4 Overapproximation of Synchronous Traces
	5 Monitoring Algorithm
	6 Experimental Evaluation
		6.1 Research Questions
		6.2 Experimental Setup
		6.3 Discussion
	7 Conclusion
	References
Author Index