自动合成紧凑防护罩，保障连续状态系统的安全运行
Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems
- 基于状态空间划分与仿真近似，求解双人安全博弈
- 通过决策树压缩策略表示，存储量减少显著
- 适合需要形式化安全保障的复杂动态系统设计
我们提出 Uppaal Coshy，一个用于在连续状态空间和复杂混合动力系统上自动合成安全策略（即防护罩）的工具。该方法通过划分状态空间并求解两人安全博弈来实现，涉及混合系统可达性等算法难题。其核心思想是利用仿真近似难以获取的精确解。该工具完全自动化，支持 Uppaal 模型的丰富形式化表达，涵盖随机混合自动机。基于划分的精度依赖于更细的网格，但存储效率低。为此，我们引入名为 Caap 的算法，以决策树形式高效生成紧凑的防护罩表示，实现显著压缩。
原文摘要 · Abstract (English)
We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy -- or shield -- for Markov decision processes over continuous state spaces and complex hybrid dynamics. The general methodology is to partition the state space and then solve a two-player safety game, which entails a number of algorithmically hard problems such as reachability for hybrid systems. The general philosophy of Uppaal Coshy is to approximate hard-to-obtain solutions using simulations. Our implementation is fully automatic and supports the expressive formalism of Uppaal models, which encompass stochastic hybrid automata. The precision of our partition-based approach benefits from using finer grids, which however are not efficient to store. We include an algorithm called Caap to efficiently compute a compact representation of a shield in the form of a decision tree, which yields significant reductions.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。