Runtime Monitoring of Supermartingale Certificates
Not on the map. Why?
Abstract (arXiv)
Supermartingale certificates formally guarantee temporal properties of discrete and continuous-time stochastic dynamical systems. However, these guarantees rely on a mathematical model of the world, leaving a sim-to-real gap that can invalidate them for the deployed system. We formulate the runtime monitoring problem for supermartingale certificates, in which a monitor observes a single system trajectory and raises an alarm when there is sufficient statistical evidence that the supermartingale certificate has been violated during execution. We present an algorithm to automatically construct a monitor using betting-based sequential tests that bound the probability of ever raising a false alarm at a user-specified level. Within this betting framework, we formulate strategies that allow the monitor to exploit spatial regularity to improve detection power while preserving this statistical guarantee. We demonstrate the efficacy of our approach on supermartingale certificate benchmarks from the literature.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 27 of its 44 references that are in the map. First posted on arXiv 14 Oct 2026.
Builds on
27 of 44 references.
References · 27
- 2017Domain Randomization for Transferring Deep Neural Networks from Simulation to the Real Worldcited by 1,498
- 2020Sim-to-Real Transfer in Deep Reinforcement Learning for Robotics: a Surveycited by 413
- 2020Estimating means of bounded random variables by bettingcited by 169
- 2022Game-theoretic statistics and safe anytime-valid inferencecited by 155
- 2022Conformal Prediction for STL Runtime Verificationcited by 35
- 2021Stability Verification in Stochastic Control Systems via Neural Network Supermartingalescited by 26
- 2022Learning Control Policies for Stochastic Systems with Reach-avoid Guaranteescited by 23
- 2023Compositional Policy Learning in Stochastic Control Systems with Formal Guaranteescited by 14
- 2024Stochastic Omega-Regular Verification and Control with Supermartingalescited by 11
- 2025On Continuous Monitoring of Risk Violations under Unknown Shiftcited by 10
- 2016Termination Analysis of Probabilistic Programs through Positivstellensatz'scited by 8
- 2016Stochastic Invariants for Probabilistic Terminationcited by 8
15 more
- 2022Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systemscited by 5
- 2024Neural Continuous-Time Supermartingale Certificatescited by 5
- 2025Quantitative Supermartingale Certificatescited by 5
- 2025Supermartingale Certificates for Quantitative Omega-regular Verification and Controlcited by 5
- 2024Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificatescited by 4
- 2022Reach-Avoid Analysis for Polynomial Stochastic Differential Equationscited by 3
- 2024PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systemscited by 3
- 2024Sound and Complete Proof Rules for Probabilistic Terminationcited by 3
- 2024Diagnostic Runtime Monitoring with Martingalescited by 3
- 2024Neural Control and Certificate Repair via Runtime Monitoringcited by 3
- 2025A Hierarchy of Supermartingales for ω-Regular Verificationcited by 3
- 2024Predictive Monitoring of Black-Box Dynamical Systemscited by 2
- 2025Formal Verification of Neural Certificates Done Dynamicallycited by 1
- 2025Alignment Monitoringcited by 1
- 2026Complete ω-Regular Supermartingale Certificatescited by 1
Built on by
Not cited yet.