PaperlayerView exact revision on arXiv

Source-linked AI summary

Runtime Monitoring of Supermartingale Certificates

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

arXiv:2610.19701v1cs.AIcs.SYeess.SY

TL;DR

Design-time model deviations can invalidate supermartingale certificate guarantees after deployment. The paper constructs a runtime monitor using betting-based sequential tests, then reports detection under changed dynamics and improved detection of local violations when exploiting temporal and spatial regularity.

  • Problem

    Supermartingale certificate guarantees depend on a design-time model, which may not match the deployed environment.

    Source: §1 · p. 1

  • Method

    The framework monitors a single stream of system states with betting-based strategies and bounds the probability of ever raising a false alarm at a user-specified level.

    Source: §1 · p. 2, §2 · p. 4, §3.2 · p. 6

  • Results

    Across benchmarks, the framework detects violations under changed deployment dynamics, and temporal and spatial regularity improves detection of local violations.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The framework bounds the probability of ever raising a false alarm and applies to discrete- and continuous-time systems and a broad range of supermartingale certificates.

    Source: §1 · p. 2, §6 · p. 11

    The monitor assumes it can compute finite bounds on accumulated allowed drift and loss from observations, and that specified random variables are integrable.

    Source: §3.1 · p. 5

Abstract

from arXiv · show

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.

1 Introduction

The introduction presents runtime monitoring as a response to model-dependent certificate guarantees that may fail after deployment. It proposes sequential betting tests and reports that temporal and spatial regularity can improve detection of local violations.

1 Introduction

  • Supermartingale certificates reduce global temporal-property reasoning to checking a local expected-decrease condition at each system step.They are probabilistic analogues of Lyapunov and barrier functions in control and inductive invariants and progress measures in software.Source: §1 · p. 1
  • Existing certificate guarantees depend on a design-time model, so environmental changes, distribution shifts, or unmodelled physical conditions can invalidate them after deployment.The paper frames this mismatch as the sim-to-real gap.Source: §1 · p. 1
  • A monitor observes a single stream of states and tests whether the certificate’s expected-decrease condition remains satisfied, alarming when statistical evidence indicates invalidity.Individual certificate-value increases or decreases do not by themselves establish violation or satisfaction in a stochastic environment.Source: §1 · p. 2
  • Across benchmarks, the framework detects certificate violations under changed deployment dynamics, while temporal and spatial regularity improves detection of local violations.The evaluated strategies weight past observations uniformly or favour recent observations and nearby states.Source: §1 · p. 2
  • The framework applies to discrete- and continuous-time systems and broad classes of supermartingale certificates, with a user-specified bound on false alarms over an unbounded monitoring horizon.The framework is agnostic to the temporal property being certified.Source: §1 · p. 2

2 Runtime monitoring of supermartingale certificates

This section formalizes the system, certificate, and monitor, then states the goal of detecting expected-decrease violations while bounding the chance of any false alarm across sampling times.

Markov Process

  • The system is modeled as a Markov process in discrete or continuous time, with the stated continuous-time setting assuming right-continuous paths and a complete, right-continuous filtration.The time domains are non-negative integers in discrete time and non-negative reals in continuous time.Source: §2 · pp. 2–3

Supermartingale Certificate

  • A supermartingale certificate is a measurable state function subject to domain-bound and expected-decrease conditions, with the latter bounding expected change or instantaneous drift from above.Continuous-time certificates require additional regularity assumptions.Source: §2 · p. 3
  • The unified certificate conditions encompass ranking supermartingales, stochastic barrier functions, reach-avoid supermartingales, and other certificates for temporal properties.The cited examples include certificates for reachability, safety, reach-avoidance, and omega-regular specifications.Source: §2 · p. 3

Example 1

  • In the robot example, setting a = 0 makes f(x) = x a ranking supermartingale, whereas every a > 0 violates the expected-decrease condition on positions (3, 7).The example models a robot whose probability of slipping increases on a sloping section of its route.Source: §2 · p. 3

Trajectory and Monitor

  • A monitor samples time-state pairs from a trajectory and applies a verdict rule to decide whether to raise an alarm.Its sampling rule selects the next observation time, and its verdict rule returns an alarm or no alarm for the sampled trajectory.Source: §2 · pp. 3–4

Problem Statement

  • The monitor must maximize alarm accuracy while ensuring that, when the certificate conditions hold, the probability of ever raising an alarm is at most δ.The bound applies over all sampling times, not separately to each observed state.Source: §2 · p. 4

Challenge

  • Monitoring domain-bound conditions is straightforward: alarm when a state lies in the domain but its certificate value falls outside the specified interval, yielding zero false alarms.The section identifies expected-decrease conditions as the main monitoring challenge.Source: §2 · p. 4
  • The construction focuses on expected-decrease monitoring, using fixed observation times and bounding alarms before any completed interval has positive conditional expected corrected drift.The statement introduces accumulated allowed drift and conditional expected corrected drift.Source: §2 · p. 4

3 Runtime monitoring as betting-based sequential testing

The monitor converts observations into bounded scores and bets sequentially on them, using a wealth threshold to control false alarms. Its betting strategies weight past scores by temporal and spatial proximity to improve detection power.

3 Runtime monitoring as betting-based sequential testing

  • The betting-based framework transforms observed states into scores, uses an abstract monitor valid for admissible strategies, and instantiates it with strategies designed to improve detection power.When the certificate condition holds, Ville’s inequality bounds the probability of ever crossing the alarm threshold by δ.Source: §3 · pp. 4–5

3.1 Scoring schemes

  • Corrected certificate changes are normalized into scores that indicate excess drift, are bounded below by −1, and have nonpositive conditional mean when the expected-decrease condition holds.The monitor subtracts an upper bound on allowed drift and divides by a loss bound computed before the next observation.Source: §3.1 · p. 5

3.2 Runtime monitoring under general betting strategies

  • Successive score bets update expert wealth, while fixed-weight mixtures and reserve-funded launches combine strategies without adding capital; the monitor alarms when total wealth reaches 1/δ.The total wealth includes the remaining reserve and the wealth of funded mixtures.Source: §3.2 · pp. 6–7
  • The monitor alarms before expected-decrease violations with probability at most δ; if a violation persists for sufficiently many observation intervals, it alarms by s+N with conditional probability at least 1−γ.Here, ε is a lower bound on the expected score at each observation.Source: §3.2 · p. 7

3.3 Weighted prediction strategies

  • Experts weight retained scores by temporal and spatial proximity, and log-return or moment stakes use those weighted histories to accommodate different violation patterns.Recent observations and observations starting near the current state receive greater weight; uniform weights result when both scales are infinite.Source: §3.3 · p. 8

4 Experimental Evaluation

Across control and neural benchmarks, monitors detect violations under changed dynamics, with spatial prediction particularly effective for localized failures. The best temporal or spatial scale depends on the violation pattern, while mixing scales often approaches the best scale.

Benchmarks and monitors

  • The evaluation spans six synthetic benchmark families, three control systems, and 16 learned controller–certificate pairs under modified deployment dynamics.Control benchmarks provide exactly computable expected certificate increments as ground truth; monitors use uniform, temporal, or spatial prediction schemes.Source: §4 · p. 9

RQ1: Detection of certificate violations

  • In Building, S-L detects every run, with median delay falling from 3043 to 732 observations as violations strengthen and become more frequent; weaker, less frequent Tanks violations remain harder to detect.With a 5% LQR control-input reduction, each monitor detects fewer than half the runs; at 20%, all detect every run.Source: §4 · p. 9, Table 1 · p. 10
  • On control benchmarks, S-L alarms on 83.8% of runs, versus 29.7% for U-L and 28.2% for T-L; on neural benchmarks at ϵ = 0, S-L alarms on 43.1%, versus approximately 11% for either baseline.The reported higher alarm rates at positive ϵ test stronger decrease requirements on the same trajectories.Source: §4 · p. 9

RQ2: Temporal vs. spatial scaling impact

  • Uniform scaling suffices for long persistent violations but struggles with transient ones; temporal and spatial weighting detect transient behavior, and spatial weighting benefits from recurrent observations.The uniform monitor’s median delay on persistent violations is 2126 observations, on par with large spatial and temporal scales.Source: §4 · p. 9
  • On the stochastic ring, the medium spatial monitor’s median delay is 640 observations versus 2360 for uniform; on temporary faults, only the medium temporal monitor alarms in more than half the cases among individual scales.Table 2 reports median detection delays across six synthetic benchmark families; NR means fewer than 25 runs alarm.Source: §4 · p. 10, Table 2 · p. 10

5 Related work

The paper distinguishes its approach from runtime monitors that detect violations directly and from predictive monitors with finite horizons. It applies betting-based sequential testing to supermartingale certificates and exploits temporal and spatial regularity to improve detection power.

Runtime monitoring of supermartingales

  • Unlike deterministic Lyapunov monitoring, a supermartingale’s required decrease holds only in expectation, so a single transition cannot establish whether the condition is satisfied.The paper applies betting-based sequential testing to this challenge for temporal properties.Source: §5 · p. 11

Betting-based testing

  • The approach uses betting-based sequential tests and temporal and spatial regularity to make informed bets and improve detection power.The paper situates supermartingale certificates within probabilistic program verification and stochastic control applications.Source: §5 · pp. 10–11

Runtime monitoring

  • Existing runtime monitors typically detect violations directly from observed states, while predictive monitoring forecasts future states but remains limited to finite horizons.The paper contrasts its certificate monitoring with these approaches and with methods that detect distribution shifts without checking certificate validity.Source: §5 · p. 11

6 Conclusion

The conclusion presents a runtime-monitoring framework for supermartingale certificates across discrete- and continuous-time systems, with a bound on the probability of ever raising a false alarm. The authors also report AI assistance in several stages of the work and take responsibility for its final content.

6 Conclusion

  • The framework monitors supermartingale certificates for temporal properties in discrete- and continuous-time systems and bounds the probability of ever raising a false alarm by a given threshold.The experiments demonstrate practical effectiveness for detecting certificate violations in stochastic control tasks.Source: §6 · p. 11
  • The authors identify shielding and repair procedures using monitor alarms as future-work directions.Source: §6 · p. 11

AI use statement

  • ChatGPT assisted with writing, literature search, theoretical development, and experimental design and implementation; the authors take responsibility for the final text, claims, proofs, references, code, and results.Source: AI use statement · p. 12

A Continuous Time

The continuous-time treatment converts an instantaneous expected-drift condition into a bound on certificate changes between fixed observation times. Its assumptions handle exits from the monitored region, while the proof decomposes corrected increments into a martingale increment and nonpositive accumulated drift difference.

Termination

  • The process is absorbed at its first actual exit from S, including exits between observations, and retains its terminal state so an exit is detectable at the next observation.The allowed drift is extended by zero outside S; termination itself does not raise a statistical alarm.Source: A Continuous Time · pp. 17–18

Continuous-time assumptions

  • The continuous-time assumptions require a right-continuous Markov process, a generator identity, and finite-horizon integrability to support the interval-increment argument.The generator drift is zero outside S, and the integrability conditions ensure the certificate and allowed drift are integrable.Source: A Continuous Time · p. 17

Proof of Lemma 3

  • Subtracting accumulated actual drift leaves a martingale; subtracting allowed drift then yields a martingale increment plus a nonpositive integrated drift difference.Conditional expectation therefore leaves only the nonpositive drift contribution to the corrected increment.Source: A Continuous Time · pp. 17, 19, 20

Observations

  • The monitor samples at fixed times and uses an observation filtration contained in the process filtration; sampled-state measurability makes the loss bound predictable.These conditions let the proof condition the martingale identity on the monitor’s available information.Source: A Continuous Time · pp. 17–18

Bounds at termination

  • Allowed drift stops accumulating at termination, the terminating interval is scored using the retained terminal state, and later intervals have zero allowance.Without the exact termination time, the piecewise bound avoids underestimating allowance when the constant drift bound is negative.Source: A Continuous Time · p. 18

Continuous-time expected increments

  • Under the continuous-time assumptions and the expected drift condition, the certificate is integrable and its corrected expected increment between successive observation times is nonpositive.The proof establishes this by showing the accumulated drift difference is nonpositive almost surely and taking conditional expectations.Source: A Continuous Time · pp. 18–20

B Validity

The validity argument turns the certificate’s expected-decrease condition into nonpositive conditional score means, then uses betting wealth to control alarms. The guarantee extends to composed monitors through an aggregate false-alarm budget.

Score decrease

  • Subtracting an upper bound on allowed drift and normalizing by a predictable positive bound preserves the sign of the score’s conditional mean.The lower loss bound ensures the resulting scores are at least −1.Source: B Validity · p. 20

False-alarm proof

  • Freezing scores at the first positive conditional expected corrected drift yields auxiliary wealth that supports a Ville-inequality bound on alarms.The auxiliary scores match the actual scores before freezing and are zero afterward.Source: B Validity · pp. 20, 22

Monitoring several conditions

  • For multiple continuous-time drift conditions with different regions, each component needs observations stopped at its own first exit, including the exit state, or another valid interval construction.One physical termination time suffices when the conditions share a continuation region.Source: B Validity · p. 23

Composition

  • If all certificate conditions hold, composing their monitors with levels summing to at most δ bounds the probability of any alarm by δ.Independence between component monitors is not required.Source: B Validity · p. 23

C Power

The power analysis develops weighted betting strategies that use historical scores and regularity-informed prediction, then gives sufficient evidence and duration conditions for alarms. Detection depends on sustained excess drift after accounting for slack, while the log-return strategy’s historical advantage does not ensure better next-step performance.

Weighted stakes

  • The log-return strategy achieves at least the moment strategy’s weighted historical log return, but neither strategy is necessarily better for the next score.A positive expected log return requires a positive conditional mean and finite conditional second moment.Source: C Power · p. 24

Locality

  • With valid regularity guesses and cutoff or linear kernels, positive prediction weights select observations whose conditional means are close to the current mean.When the current mean is sufficiently positive, selected observations also have positive means; realized scores can still be negative, and geometric kernels do not ensure this implication.Source: C Power · p. 25

Sufficient evidence

  • An expert’s accumulated evidence suffices for an alarm once its contribution reaches the threshold; with stakes at most 1/2, a quadratic lower-bound condition also suffices.Dividing capital among experts raises the individual evidence threshold, although other accounts may trigger an alarm sooner.Source: C Power · p. 26

Persistent violations

  • Under a blockwise excess-drift condition, the monitor raises an alarm by s + N with conditional probability at least 1 − β.The excess must exceed expected slack, and the sufficient duration grows quadratically as that excess shrinks.Source: C Power · pp. 27, 29

D Implementation

The implementation updates betting accounts from a retained history of completed scores and starting states, checks total wealth against the alarm threshold, and can aggregate accounts under shared-strategy conditions. Storage and per-observation work depend on the history size and expert set, with a separate optimization for certain unlimited-history moment strategies.

Algorithm 1

  • At each observation, the monitor chooses funding and stakes from available information, computes the new score, updates accounts, and alarms if total wealth reaches 1/δ.It then appends the completed score and starting state to the history, retaining the most recent m entries.Source: D Implementation · pp. 29–30

Combining accounts

  • When launches share a fixed expert set, weights, and stakes, their accounts can be combined without changing total wealth or alarm time.Accounts whose scales or prediction histories depend on launch time generally must remain separate.Source: D Implementation · p. 30

Computational cost

  • For d-dimensional states, storage is O(md + K); per-observation work is O(md + Km) for moment stakes and O(md + KmJ) for log-return stakes using J bisection iterations.These bounds exclude resources required by the certificate, score-bound, and funding routines.Source: D Implementation · pp. 30–31

Recursive updates for unlimited history

  • Uniform or temporal-geometric moment strategies can use unlimited history with O(K) work and storage per observation.This optimization generally does not extend to spatial weights or exact log-return optimization.Source: D Implementation · p. 31

E Experimental setup

The setup compares uniform, temporal, and spatial prediction strategies using specified histories, scales, mixtures, and account-launch schedules. Synthetic benchmarks use a longer retained history than the control and neural benchmarks.

Prediction strategies

  • Uniform prediction weights retained scores equally, temporal prediction favors recent scores, and spatial prediction favors scores from nearby starting states.Temporal and spatial prediction use linear kernels with fixed scales.Source: E Experimental setup · p. 31

Synthetic benchmarks

  • Synthetic benchmarks retain 16384 observations and test five scales calibrated to effective sample sizes 32, 128, 512, 2048, and 8192.The setup also evaluates individual scales, equal and centered mixtures, and mixtures omitting one scale; temporal cutoffs range from approximately 43.166 to 10923.167 observations.Source: E Experimental setup · p. 31

Control and neural benchmarks

  • Control and neural benchmarks use U-L, T-L, and S-L with 8192 observations; accounts launch every 256 observations.T-L mixes temporal cutoffs 64, 128, 512, 2048, and 8192, while S-L mixes spatial radii 0.00625, 0.025, 0.1, 0.4, and 1.6.Source: E Experimental setup · p. 31

E.1 Synthetic benchmarks

The synthetic benchmarks isolate persistent, delayed, temporary, and recurring local violations across six process families. Their settings vary violation strength, timing, duration, and recurrence.

E.1 Synthetic benchmarks

  • Six synthetic process families isolate distinct sources of detection difficulty, including persistent, delayed, temporary, and recurring local violations.Source: §E.1 · p. 31
  • Scalar-process violations vary in magnitude, onset, and duration, with runs lasting 32,768 observations.Persistent corrected-drift means are 0.01, 0.02, or 0.05; delayed and temporary cases change the mean at specified onsets or durations.Source: §E.1 · pp. 31–32
  • Direct recurrence places 64 positive-mean observations in each period, with periods of 512, 2,048, or 4,096 and 512 exposed observations per run.The gaps between visits grow with the period.Source: §E.1 · p. 32
  • The stochastic ring varies radial feedback in a sector while radial position and angular speed are noisy, making return times and disturbance exposure vary across runs.The feedback reduction reaches 75%; periods and horizons match the direct-recurrence settings.Source: §E.1 · p. 32
  • The hill benchmark adds a state-dependent disturbance near the robot’s path, with amplitudes that reduce expected progress at the hill centre by one quarter, one half, or entirely.The robot starts at 10 and stops on reaching [0, 1].Source: §E.1 · p. 32
  • Cyclic-system periods change the horizon and retained history; the six example trajectories illustrate selected settings, while heatmaps summarise all seeds.Source: §E.1 · p. 32

E.2 Control benchmarks

The control suite evaluates Building, Two Tanks, and LQR under fixed certificates and allowances, using reference settings and disturbances at three strengths. Exact conditional moments along recorded paths support evaluation of violations and expected scores.

E.2 Control benchmarks

  • Building, Two Tanks, and LQR each have one reference setting and two disturbances at three strengths, yielding 21 settings in total.Disturbances act from the start, while certificates and allowances remain fixed.Source: §E.2 · p. 32
  • Building disturbances reduce heating effectiveness or introduce controller temperature underestimation; the monitor observes the true temperature in the latter case.The changes are 8%, 10%, or 12%, or offsets of 1, 2, or 3 degrees.Source: §E.2 · p. 32
  • Two Tanks disturbances add fading inlet flow or probabilistic inlet bursts, with bounded triangular noise and newly synthesised sum-of-squares certificates.Exact-arithmetic checks validate nominal allowances of 0.04 for Building and 0.07 for Tanks.Source: §E.2 · p. 32
  • LQR uses a standard quadratic value function, exact Gaussian transitions sampled every 0.1 time units, and disturbances to feedback or noise amplitude.Feedback reductions are 5%, 10%, or 20%; noise multipliers are 1.05, 1.10, or 1.20.Source: §E.2 · p. 33
  • Control runs stop at 32,768 observations or earlier at system-specific boundaries, and exact conditional moments are computed along each recorded trajectory.Source: §E.2 · p. 33

E.3 Neural controller–certificate pairs

The evaluation combines neural controller–certificate pairs with synthetic, control, and neural benchmark results. The figures specify how detection rates, delays, and expected-score summaries are measured across these suites.

E.3 Neural controller–certificate pairs

  • The neural suite retains 16 controller–certificate pairs across five system groups, with fixed parameters, shared initial-state pools, and three disturbance magnitudes per setting.Paths are lengthened by scaling source drift increments and direct plant-noise amplitudes by 1/20.Source: §E.3 · p. 33

F Synthetic

  • Synthetic figures report eligible first-alarm percentages and detection delays across prediction rules, scales, and stake types; expected-score summaries include recovery and later excursions.The example trajectories illustrate individual runs, whereas heatmaps summarise all seeds.Source: Figure 1 · p. 34, Figure 2 · p. 35, Figure 11 · p. 44

G Control

  • Control figures report first-alarm percentages, 50% detection delays, and per-run expected-score summaries computed from exact conditional moments.The positive-excess trajectory fraction is distinct from both the alarm rate and the fraction of observations with positive conditional excess.Source: Figure 12 · p. 45, Figure 13 · p. 46, Figure 14 · p. 47

H Neural

  • Neural figures compare first-alarm percentages and delays across disturbance strengths and decrease requirements; the conditions remain unverified under adapted dynamics, including reference settings.Delay summaries retain nondetections and short paths in the denominator, and detection depends on trajectory length as well as available evidence.Source: §E.3 · p. 33, Figure 15 · p. 48, Figure 16 · p. 49
Loading 2610.19701v1…