外观
论文arXiv 2610.1970114 天前
超鞅证书的运行时监测
原文链接:Runtime Monitoring of Supermartingale Certificates(arXiv 2610.19701 · 发布日期:2026-10-14)
Runtime Monitoring of Supermartingale Certificates
针对超鞅证书依赖模型导致部署失效的问题,提出基于投注序贯检验的运行时监测,并在文献基准上验证。
核心要点
- 超鞅证书的保证依赖世界数学模型,部署时可能出现 Sim-to-Real 间隙。
- 将运行时监测表述为观察单条轨迹,并在证书被违反有足够统计证据时报警。
- 用投注式序贯检验自动构造监测器,并按用户指定水平限制误报概率。
- 利用空间规律性的策略提升检测能力,同时保持统计保证;在文献基准展示有效性。
验证范围与局限:验证范围为文献中的超鞅证书基准。
英文摘要 (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.
作者:Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner, Emily Yu, Đorđe Žikelić
来源
本页事实对应的公开页面,以原文为准。