Runtime Monitoring of Supermartingale Certificates

Supermartingale certificates formally guarantee temporal properties of discrete and continuous-time stochastic dynamical systems. However these guarantees rely and hold within a mathematical model of the world, leaving a sim-to-real gap that can render them invalid under 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.