Runtime Monitoring of Supermartingale Certificates
Authors: Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner, Emily Yu, Đorđe Žikelić
Organizations: University of Birmingham · Institute of Science and Technology Austria · University of Oxford · Leiden University · Nanyang Technological University
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.
Figures & tables
Detections (median delay)
Benchmark & Setting
Magnitude
Exposure (%)
U-L
T-L
S-L
Building: 8% heating loss
0.0151
24.9
0 (NR)
0 (NR)
50 (3043)
Building: 12% heating loss
0.0309
37.6
0 (NR)
0 (NR)
50 (732)
Tanks: burst probability 0.35
0.00561
5.5
0 (NR)
0 (NR)
0 (NR)
Tanks: burst probability 0.45
0.00615
11.0
0 (NR)
0 (NR)
34 (28507)
LQR: 5% feedback loss
0.00955
100.0
19 (NR)
12 (NR)
16 (NR)
Table 1: Violation strength and detection in selected control settings, with 50 runs each. For each run, magnitude is the average of μn over violating observations, and exposure is the percentage of violating observations. Magnitude and exposure are reported as medians over the 50 runs. Detection entries give counts, with median delay in parentheses. Detection delay is measured in observations from violation onset or first entry into the violating region. U-L, T-L, and S-L use uniform, temporal, and spatial prediction, respectively. NR means fewer than 25 runs alarm.
Temporal prediction
Spatial prediction
Scale
Pers.
Del.
Temp.
Rec.
Ring
Hill
Scale
Pers.
Del.
Temp.
Rec.
Ring
Hill
Uniform
2126
3204
NR
NR
2360
588
Uniform
2126
3204
NR
NR
2360
588
Equal
2183
668
914
1102
664
492
Equal
3351
2141
NR
571
654
482
XS
NR
1565
NR
570
168
568
XS
NR
3979
NR
NR
NR
670
S
6719
756
NR
2110
1127
441
S
NR
2977
NR
NR
655
594
M
2442
575
766
NR
1713
476
M
21051
3437
NR
1578
640
552
Table 2: Median detection delay in observations on the six synthetic benchmark families: persistent, delayed, temporary, direct recurrence, stochastic ring, and hill. XS–XL denote extra-small through extra-large prediction scales (exact parameters given in Appendix). Temporal scales determine how far back in the history observations receive weight; spatial scales determine the neighbourhood radius around the current state. Equal divides capital equally among the five scale experts. Uniform weights all retained observations equally. NR means fewer than 25 runs alarm.
Benchmark set
No. Settings
U-L(%)
T-L(%)
S-L(%)
Synthetic
18
62.2
77.0
79.6
Control
18
29.7
28.2
83.8
Neural, ϵ=0
48
10.7
10.8
43.1
Neural, ϵ=0.0005
48
71.9
71.7
77.8
Neural, ϵ=0.001
48
76.1
76.3
81.0
Table 3: Percentage of runs in which each monitor raises an alarm, averaged across settings (50 runs per setting). For neural , ϵ=0 tests expected nonincrease; larger ϵ requires faster expected decrease.
Appendix figures & tables16 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 1: Detection rates for the synthetic benchmarks, with 21 settings, 50 monitors and 50 paired runs per setting. Cells show the percentage of runs with an eligible first alarm; reference rows count any first alarm. The panels separate moment (M) and log-return (L) stakes. U uses uniform prediction, while T and S use temporal and spatial prediction. XS–XL denote individual scales; Eq is their equal mixture; Ctr uses weights (0.1,0.2,0.4,0.2,0.1) . A minus label indicates that the corresponding scale is omitted from an otherwise equal mixture. All monitors use wealth threshold 20 . The panels share a colour scale from 0 to 100% . NA denotes incomplete data.
Figure 2: The 50% detection delays for the synthetic monitors in Figure 1 . Each value is the first delay by which 25 of all 50 runs have eligible first alarms, measured in observations since the declared onset or first entry into the region with positive conditional mean. Nondetections, short paths and early first alarms remain in the denominator. A later crossing does not replace an early first alarm. NR denotes a median that was not reached, NA incomplete data, and a dash an undefined reference delay. Both panels use the same colour scale.
Figure 3: Differences in synthetic detection rates between log-return and moment stakes, computed as L − M in percentage points. Each comparison uses the same prediction rule and the same 50 paths. Positive green cells indicate more alarms with log-return stakes; negative cells indicate more alarms with moment stakes. For reference rows, more alarms mean a higher false-alarm rate. Column labels follow Figure 1 . The comparison includes the different stake caps, 0.99 for L and 0.5 for M. These differences are descriptive; no significance test is applied.
Figure 4: Differences in synthetic median detection delays, computed as Q0.5M−Q0.5L in observations. Positive green values indicate earlier detection with log-return stakes when both strategies reach 25 eligible first alarms among all 50 runs. L only and M only indicate that only the named strategy reaches this fraction; NR means neither does. Reference delays are undefined (Ref.), and NA denotes incomplete data. No artificial delays are assigned to non-numeric cells. The comparisons use the same prediction rules and paths, with the respective stake caps of each strategy.
Figure 5: Persistent violation with g=0.01 and seed 970000003 . From top to bottom: the scalar state; mean increase g ; the exact expected certificate increment g−0.001=0.009 and allowance −0.001 ; and monitor wealth on a logarithmic scale. Uniform noise on [−0.6,0.6] makes individual increments noisy despite the positive conditional mean of the corrected increment. U uses uniform prediction, while T-equal and S-equal mix the five XS–XL experts equally. M and L denote moment and log-return stakes. The dotted line marks wealth threshold 20 . All 32768 observations are shown, including those after alarms.
Figure 6: Delayed violation with onset 8192 and seed 970000003 . The conditional mean of the corrected increment changes from −0.02 to 0.05 and remains positive. From top to bottom: the state; mean increase 0.07 ; the expected certificate increment, changing from −0.021 to 0.049 , and allowance −0.001 ; and logarithmic monitor wealth. Temporal prediction reduces the influence of observations collected before onset as new scores arrive. U, T-equal and S-equal are shown with both M and L stakes, as in Figure 5 . The wealth threshold is 20 . Neither the history nor wealth is reset at onset.
Figure 7: Temporary violation lasting 256 observations from onset 8192 , with seed 970000003 . The conditional mean of the corrected increment is 0.05 during the disturbance and −0.02 before and after it. From top to bottom: the state; temporary mean increase 0.07 ; the expected certificate increment and allowance −0.001 ; and logarithmic wealth for U and the equal T/S mixtures with M and L stakes. None of the six displayed monitors reaches the dotted threshold 20 . The path is shown through observation 32768 , including recovery. The aggregate detection summaries also count eligible first alarms occurring after recovery.
Figure 8: Direct recurrence with period P=4096 and seed 970000003 . Each of eight visits to a fixed circular sector contains 64 observations with score mean 0.10 . Between visits, the mean is −0.02 . Independent symmetric score noise has amplitude 0.3 . From top to bottom: the two state coordinates; local mean increase 0.12 ; the prescribed conditional score mean relative to zero; and logarithmic wealth for U and the equal T/S mixtures with M and L stakes. The 32768 observations include exactly 512 with positive conditional mean. Spatial prediction can reuse observations from earlier visits despite the long gaps between them. The dotted line marks wealth threshold 20 .
Figure 9: Stochastic ring with nominal period P=4096 and seed 970000003 . From top to bottom: radial error relative to the unit circle; the state-dependent reduction in restoring feedback, reaching 0.75 in the affected sector; the exact expected certificate increment minus its nominal allowance; and logarithmic monitor wealth. The certificate is the squared radial error. Radial and angular noise make return times and violation exposure vary across runs. U and the equal T/S mixtures are shown with M and L stakes. The dotted line marks wealth threshold 20 . The expected-increment condition can be violated even while the process remains close to the circle. All observations are retained, including those after alarms.
Figure 10: Hill disturbance with amplitude a=0.0625 and seed 970000003 . From top to bottom: distance to the target [0,1] , with the hill region (3,7) shaded; additional slip probability a(1−∣x−5∣/2)+ ; the exact expected certificate increment and required allowance −0.005 ; and logarithmic wealth for U and the equal T/S mixtures with M and L stakes. At x=5 , the expected increment is −0.00375 , a 25% reduction in progress. The robot therefore still approaches the target in expectation while violating the required rate of decrease. The dotted line marks wealth threshold 20 . The run ends when the robot reaches the target, not when a monitor raises an alarm.
Figure 11: Normalised expected-score summaries for the synthetic benchmarks. Each cell is the median of 50 quantities computed separately for each run: the fraction of observations with μn>0 , the signed mean of μn , its mean over positive-mean observations, and the mean of (μn)+ over all observations. Summaries start at onset or first entry and include recovery and later excursions. References use the full path. Each run receives equal weight. A hatched dash marks an undefined mean over positive observations; NA denotes incomplete data. Column colour scales match the control heatmap, with the signed scale centred at zero.
Figure 12: First-alarm percentages for Building, Two Tanks and LQR. Each system has a reference setting and two disturbances, each evaluated at three strengths. U-L, T-L and S-L use uniform, temporal and spatial prediction with log-return stakes and wealth threshold 20 . Every cell uses all 50 paired runs. The Viol. column gives the percentage of trajectories encountering at least one positive conditional excess, computed from exact model moments with tolerance 10−12 in raw units. This differs from both the alarm rate and the fraction of observations with positive conditional excess. Reference alarms measure false alarms under the validated nominal conditions.
Figure 13: The 50% detection delays for the control settings and log-return monitors in Figure 12 . Disturbances act from the start, so each entry is the number of observations until 25 of all 50 runs have raised their first alarm. NR means this fraction was not reached, and NA denotes incomplete data. Nondetections remain in the denominator. Reference delays also start at the beginning of the run and concern false alarms. LQR observations are spaced by 0.1 physical time units; all entries are reported in observations.
Figure 14: Normalised expected-score summaries for the control benchmarks, computed from exact conditional moments along each recorded path. Cells give medians of 50 equally weighted per-run summaries: the fraction of positive-mean observations, the signed mean, the mean over positive-mean observations, and the mean positive part. The last quantity includes all observations in its denominator. A negative signed mean can therefore coexist with local violations. Positivity requires a raw conditional excess above 10−12 . Reference and disturbed runs use their full paths, including observations after alarms. A hatched dash marks an undefined mean over positive observations; NA denotes incomplete data. Column colour scales match Figure 11 .
Figure 15: First-alarm percentages for the neural benchmarks. Each of the 16 original controller–certificate pairs has a reference setting and three disturbance strengths. Each row uses 50 trajectories shared by U-L, T-L and S-L and by the conditions ϵ=0,0.0005,0.001 . The allowance is −ϵ for ordinary certificates and (e−ϵ−1)f(x) for exponentiated logarithmic certificates. All monitors use wealth threshold 20 . Question marks in Viol. indicate that the conditional mean estimates at selected states do not determine the exact fraction of runs encountering a violation. All three conditions remain unverified under the adapted dynamics, including in the reference settings. Reference alarms therefore do not measure false-alarm rates under a verified null.
Figure 16: The 50% detection delays for the neural pairs, disturbances and conditions in Figure 15 , measured in observations from the start of each run. Each finite entry requires 25 first alarms among all 50 paired paths. Short paths and nondetections remain in the denominator. NR means this fraction was not reached, and NA denotes incomplete data. Paths end at the target, an unsafe set, domain exit, certificate threshold or 20480 observations. Detection therefore depends on both the evidence available and the length of the trajectory. All condition blocks share a colour scale. The different conditions change the allowance on the same physical trajectories.
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.
Zhipeng Cao, Taoran Wu, Weiru Cui +2
Institute of Software, Chinese Academy of Sciences · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · University of Chinese Academy of Sciences +1
Machine learning systems are increasingly corrected while they run, and the decision of when to intervene is increasingly delegated to statistical monitors. Anytime-valid inference promises evidence that can be acted on at any moment, exactly the guarantee this setting needs, and it is moving from theory into deployed monitoring. Conformal test martingales are the change-detection instrument, and Ville's inequality caps their false-alarm probability on exchangeable data. The guarantee is conditional. A deployment inherits it only if the stream it monitors behaves exchangeably. The premise is hardest to satisfy where these monitors are most useful, on dependent data and inside loops where the monitor modifies the learner whose scores it reads. It is also rarely measured. We measure it in a pre-specified case study, where such a monitor gates the online updates of a Kalman adapter correcting frozen time-series foundation models on five forecasting streams. On exchangeable synthetic streams, the same implementation fires in at most 1 of 60 runs. On the real streams, at alpha = 0.05, 135 of 135 clean-stream runs fired. The construction does not explain the firing; the failure comes from the deployed score stream itself. Repeated fires hold the gate's drift response active, and the gated filter amplifies the very transient it was designed to prevent. The component worth keeping makes no validity claim. Huber-style gating of the filter's own updates cuts isolated-spike degradation by an order of magnitude with no dataset specific tuning. Anytime-valid methods proposed for dependent data should therefore be accompanied by null-calibration controls and mechanism traces.
Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of ω-regular properties (and therefore of linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for ω-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an ω-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.
Alessandro Abate, Daniel Contro, Mirco Giacobbe +2
University of Oxford, UK · University of Birmingham, UK