利用可达集内外逼近的线性系统全自动验证
Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets
AI总结：
本文提出一种全自动可达性算法，通过内部自动调整参数并利用豪斯多夫距离误差界和闵可夫斯基差提取内外逼近，实现对线性系统时变安全规范的全自动验证或证伪。
摘要：
可达性分析是一种在不确定性影响下保障动力系统安全性的形式化方法。所有可达性算法的一个重大瓶颈在于必须充分调整特定算法参数（例如时间步长），而这需要专业知识。在本工作中，我们通过一种全自动可达性算法解决了这一问题，该算法在内部调整所有算法参数，使得可达集包络在豪斯多夫距离意义下满足用户定义的相对于精确可达集的逼近误差界。此外，该误差界可用于利用闵可夫斯基差从外逼近中提取可达集的内逼近。最后，我们提出一种新的验证算法，该算法自动细化外逼近和内逼近的精度，直到由时变安全集和不安全集给出的规范能够被验证或证伪。数值评估表明，我们的验证算法无需手动调参即可成功验证或证伪来自不同领域的基准测试。
英文摘要：
Reachability analysis is a formal method to guarantee safety of dynamical systems under the influence of uncertainties. A substantial bottleneck of all reachability algorithms is the necessity to adequately tune specific algorithm parameters, such as the time step size, which requires expert knowledge. In this work, we solve this issue with a fully automated reachability algorithm that tunes all algorithm parameters internally such that the reachable set enclosure respects a user-defined approximation error bound in terms of the Hausdorff distance to the exact reachable set. Moreover, this bound can be used to extract an inner-approximation of the reachable set from the outer-approximation using the Minkowski difference. Finally, we propose a novel verification algorithm that automatically refines the accuracy of the outer-approximation and inner-approximation until specifications given by time-varying safe and unsafe sets can be verified or falsified. The numerical evaluation demonstrates that our verification algorithm successfully verifies or falsifies benchmarks from different domains without requiring manual tuning.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
