基于可达集内外逼近的线性系统全自动化验证

可达性分析是在不确定性影响下保证动力系统安全性的形式化方法。所有可达性算法的一个实质性瓶颈是必须充分调优特定算法参数(如时间步长)，这需要专家知识。在本工作中，我们解决了这一问题：提出一种全自动可达性算法，其在内部调优所有算法参数，使得可达集包围体相对于精确可达集的 Hausdorff 距离满足用户定义的逼近误差界。此外，该误差界可用于通过 Minkowski 差从外逼近中提取可达集的内逼近。最后，我们提出一种新颖的验证算法，自动细化外逼近与内逼近的精度，直至可由时变安全集与不安全集给出的规范被验证或证伪。数值评估表明，我们的验证算法无需手动调参即可成功验证或证伪来自不同领域的基准问题。