Uppaal Coshy：用于混合系统的紧凑护罩自动合成

我们提出 Uppaal Coshy，这是一个用于自动合成安全策略（即护罩）的工具，适用于连续状态空间和复杂混合动力学的马尔可夫决策过程。通用方法是划分状态空间，然后求解两人安全游戏，这涉及诸多算法上的困难问题，如混合系统的可达性。Uppaal Coshy 的通用思想是通过仿真来近似获取困难的解。我们的实现是全自动的，并且支持 Uppaal 模型的表达丰富的形式，这些模型涵盖了随机混合自动机。我们基于划分的分层方法的精度受益于使用更细的网格，但后者在存储方面并不高效。我们包含一种称为 Caap 的算法，用于高效计算护罩的紧凑表示形式，呈现为决策树，从而实现显著的减小。