动态验证神经证书，实时检测安全违规，无需访问控制策略。
Formal Verification of Neural Certificates Done Dynamically
- 运行时监控系统状态，实时验证证书有效性
- 在有限预测期内检测到安全违规，延迟低且开销小
- 适用于部署阶段的安全保障，适合嵌入式系统应用
神经证书已成为网络物理系统控制中的有力工具，可作为系统正确性的证据。这类证书（如屏障函数）通常与控制策略共同学习，经验证后可提供系统安全的数学证明。然而，传统形式化验证其定义条件常因需穷尽状态空间探索而面临可扩展性挑战。为此，我们提出一种轻量级运行时监控框架，集成实时验证，无需访问底层控制策略。该监控器在系统部署期间观察运行状态，并对前瞻区域内的证书进行即时验证，确保在有限预测期内的安全性。我们以基于ReLU的控制屏障函数为例实现该框架，并在案例研究中验证了其实际有效性。该方法能及时发现安全违规和错误证书，开销极小，为证书的静态验证提供了高效且轻量的替代方案。
原文摘要 · Abstract (English)
Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。