Anytime-Valid Runtime Monitoring of Learned Barrier Certificates
Authors: Zhipeng Cao, Taoran Wu, Weiru Cui, Luke Ong, Bai Xue
Organizations: Institute of Software, Chinese Academy of Sciences · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · University of Chinese Academy of Sciences · College of Computing and Data Science, Nanyang Technological University
Learned barrier certificates provide a principled mechanism for establishing safety of stochastic systems, but their validity may deteriorate during deployment when the underlying dynamics differ from those used for training. We propose an anytime-valid runtime monitor that audits a learned barrier certificate using observed closed-loop trajectories. The monitor is intended to detect loss of statistical support for the deployed barrier condition; it does not by itself guarantee detection before unsafe entry or safety of a subsequent intervention. Specifically, the conditional barrier-drift condition is formulated as an episode-wise sequential hypothesis test, and observed barrier increments are transformed into a nonnegative test supermartingale, yielding finite-sample false-alarm control under arbitrary stopping times. Inspired by finite-horizon safety verification, we further introduce a deterministic temporal shaping of the monitoring boundary, making the monitor more conservative early in a prescribed deployment horizon while preserving anytime-validity. The monitor is designed to detect statistical evidence that the safety certificate is no longer consistent with the observed dynamics, rather than to predict unsafe entry. To assess the monitor empirically, we evaluate empirical alarm behavior under valid and invalid certificates. Code and data are available at https://github.com/FormalCert-AI/runtime-barrier-monitor.
Figures & tables
Figure 1: Overview of the proposed framework for anytime-valid monitoring of learned barrier certificates.
Direct
DAB
System
Kmaxlna
ρα
p^max
ρα
p^max
Valid certificates
System 1
0
0.00
4.80
0.00
0.90
4
0.00
0.20
0.00
0.10
System 2
0
0.00
0.00
0.00
0.00
4
0.00
0.00
0.00
0.00
Table 1: Runtime monitoring under valid and invalid certificates with Kmaxlna=0 and the default setting Kmaxlna=4 on the same runs. ρα is the fraction of initial states with p^i>α and p^max=maxip^i is the worst-case alarm rate. N=103 initial states, R=103 trajectories per initial state, Kmax=400 , α=0.05 . All values are percentages. Figure 3 shows the full distribution of p^ .
Figure 2: The trade-off between avoiding unnecessary alarms and detecting degradation promptly.
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 3: Distribution of the alarm rate p^i over the N=103 initial states, Direct (left half) against DAB (right half), with the standard rule Kmaxlna=0 (top row) and the default Kmaxlna=4 (bottom row); the row below each axis holds the share of initial states with p^i=0 .
Figure 4: Effect of the patience parameter a on the DAB alarm rates and evidence for the invalid certificates.
Figure 5: Initial barrier value B(x0) and alarm rate: solid lines and filled markers for the standard rule Kmaxlna=0 , dashed lines and hollow markers for the default Kmaxlna=4 .
Betting rules
Bet λt
Alarm
Guar.
Direct
1/Bt
Mt≥αaKmax−t
✓
Fraction mix.
c/Bt,c∈C
Mˉt≥αaKmax−t
✓
Absolute mix.
min{β,1/Bt},β∈Aj
Mˉt≥αaKmax−t
✓
DAB
Eq. 4
Mt≥αaKmax−t
✓
Appendix
Table 2: Compared betting rules, all driven by the increments δt=Bt−Bt−1 . Guar.: PH0(τ≤Kmax∣x0)≤α for every x0 (Theorem 1 ).
Direct
Fraction mix.
Absolute mix. A1
Absolute mix. A2
DAB
System
ρα
p^max
ρα
p^max
ρα
p^max
ρα
p^max
ρα
p^max
Valid certificates
System 1
0.00
0.20
0.00
0.50
0.00
0.00
0.00
0.00
0.00
0.10
System 2
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
Invalid certificates
System 2-input attack
17.90
100.00
11.30
100.00
0.00
0.00
0.00
1.20
79.90
81.50
Appendix
Table 3: Comparison with other monitors on the runs of Table 1 . N=103 initial states, R=103 trajectories per initial state, Kmax=400 , Kmaxlna=4 , α=0.05 . All values are percentages.
Figure 6: Distribution of the alarm rates p^i over the initial states for all monitors ( Kmaxlna=4 ).
Figure 7: Sensitivity to the horizon Kmax , DAB memory γ and DAB cap U .
Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.
Safety of stochastic dynamic systems in environments with dynamic obstacles is studied in this paper through the lens of stochastic barrier functions. We introduce both time-invariant and time-varying barrier certificates for discrete-time, continuous-space systems subject to uncertainty, which provide certified lower bounds on the probability of remaining within a safe set over a finite horizon. These certificates explicitly account for time-varying unsafe regions induced by obstacle dynamics. By leveraging Bellman's optimality perspective, the time-varying formulation directly captures temporal structure and yields less conservative bounds than state-of-the-art approaches. By restricting certificates to polynomial functions, we show that time-varying barrier synthesis can be formulated as a convex sum-of-squares program, enabling tractable optimization. Empirical evaluations on nonlinear systems with dynamic obstacles show that time-varying certificates consistently achieve tight guarantees, demonstrating improved accuracy and scalability over state-of-the-art methods.
Rayan Mazouz, Luca Laurenti, Morteza Lahijanian
Dept. of Aerospace Eng. Sciences at University of Colorado Boulder, USA · Delft University of Technology, The Netherlands
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.
Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner +2
University of Birmingham · Institute of Science and Technology Austria · University of Oxford +2