用概率代理模型提升不确定系统的形式化控制可扩展性
Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)
- 基于概率仿真关系构建代理模型，避免直接计算误差界
- 在高维非线性系统中实现无限时域时序逻辑验证
- 适合复杂自动驾驶场景的形式化验证与设计
准确建模系统的需求不仅难以实现，还限制了形式化方法的可扩展性，因为生成的模型往往过于复杂，难以支持有效决策并保证形式正确性和性能。针对随机系统中的概率仿真关系与代理模型，我们提出一种新方法，显著提升了此类仿真关系的可扩展性和实用性，无需直接计算误差边界。该方法实现了基于抽象的高效技术，在高维空间中仍能有效处理复杂的非线性智能体-环境交互，并在不确定性下提供无限时域时序逻辑保障。在复杂的高维车辆交叉口案例研究中，验证了该方法在保持合理保守性的同时，显著提升可扩展性。
原文摘要 · Abstract (English)
The requirement for identifying accurate system representations has not only been a challenge to fulfill, but it has compromised the scalability of formal methods, as the resulting models are often too complex for effective decision making with formal correctness and performance guarantees. Focusing on probabilistic simulation relations and surrogate models of stochastic systems, we propose an approach that significantly enhances the scalability and practical applicability of such simulation relations by eliminating the need to compute error bounds directly. As a result, we provide an abstraction-based technique that scales effectively to higher dimensions while addressing complex nonlinear agent-environment interactions with infinite-horizon temporal logic guarantees amidst uncertainty. Our approach trades scalability for conservatism favorably, as demonstrated on a complex high-dimensional vehicle intersection case study.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。