LLM2D
基于状态空间变换的高效屏蔽合成
Efficient Shield Synthesis via State-Space Transformation
作者: Asger Horn Brorholt, Andreas Holck H{\o}eg-Petersen, Kim Guldstrand Larsen, Christian Schilling
发布日期: 10/8/2024
arXiv ID: oai:arXiv.org:2407.19911v4

摘要

我们研究了为控制系统合成安全策略(也称为防护罩)的问题。由于状态空间是无限的,防护罩通常是在有限状态抽象上计算的,最常见的抽象是矩形网格。然而,对于许多系统而言,这种网格并不能很好地与安全属性或系统动力学相匹配。这就是为什么粗网格很少足够,而精细网格通常在计算上不可行的原因。在本文中,我们表明适当的状态空间变换仍然允许使用粗网格,几乎没有计算开销。我们在三个案例研究中证明了我们的基于变换的合成比标准合成快几个数量级。在前两个案例研究中,我们使用领域知识来选择合适的变换。在第三个案例研究中,我们报告了在没有领域知识的情况下设计变换的结果。