Runtime Monitoring of Supermartingale Certificates

Mirco Giacobbe; Thomas A. Henzinger; Konstantin Kueffner; Emily Yu; Đorđe Žikelić

cs.AIOct 14, 2026

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 ·

Abstract

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

\mu_{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, $\epsilon=0$	48	10.7	10.8	43.1
Neural, $\epsilon=0.0005$	48	71.9	71.7	77.8
Neural, $\epsilon=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 ,

\epsilon=0

tests expected nonincrease; larger

\epsilon

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 $Q_{0.5}^{\mathrm{M}}-Q_{0.5}^{\mathrm{L}}$ 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

0.05

and remains positive. From top to bottom: the state; mean increase

0.07

; the expected certificate increment, changing from

-0.021

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

\mu_{n}>0

, the signed mean of

\mu_{n}

, its mean over positive-mean observations, and the mean of

(\mu_{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 $\epsilon=0,0.0005,0.001$ . The allowance is $-\epsilon$ for ordinary certificates and $(e^{-\epsilon}-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.

Runtime Verification

Runtime verification checks executing systems against formal properties to detect, predict, or prevent violations.

See all 62 papers

Anytime-Valid Runtime Monitoring of Learned Barrier Certificates
Oct 20, 2026Zhipeng Cao, Taoran Wu, Weiru Cui +2Runtime Verification Control Barrier Functions
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
When the Martingale Never Stops Firing: Anytime-Valid Gating on Real Forecast Streams
Aug 31, 2026Weijia Han, Lisha QuAnytime-Valid Inference Conformal Prediction
University of Washington · Seattle, USA
Value Functions as Supermartingale Certificates
May 29, 2026Alessandro Abate, Daniel Contro, Mirco Giacobbe +2Formal Methods for RL Reinforcement Learning
University of Oxford, UK · University of Birmingham, UK

Oct 20, 2026J/K move · Enter open · S save

Anytime-Valid Runtime Monitoring of Learned Barrier Certificates

Zhipeng Cao, Taoran Wu, Weiru Cui, Luke Ong+1

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

Runtime Verification Control Barrier Functions Anytime-Valid Inference

Open paper AskPDF arXiv

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.

Abstract

Runtime Verification

Explore similar work

Anytime-Valid Runtime Monitoring of Learned Barrier Certificates

When the Martingale Never Stops Firing: Anytime-Valid Gating on Real Forecast Streams

Value Functions as Supermartingale Certificates