论文标题
使用可触及集的内部和外表示例对线性系统的完全自动验证
Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets
论文作者
论文摘要
可及性分析是一种正式的方法，可以在不确定性的影响下确保动态系统的安全性。所有可及性算法的大量瓶颈是需要充分调整特定算法参数的必要性，例如时间步长，需要专家知识。在这项工作中，我们使用完全自动化的可及性算法来解决此问题，该算法在内部调整所有算法参数，以使可触及的设置围栏尊重用户定义的近似差异，该近似误差以Hausdorff距离限制到确切的可触及设置。此外，该结合可用于使用Minkowski差异从外部应用程序中提取可触及的集合的内部贴合。最后，我们提出了一种新型的验证算法，该算法会自动完善外部附属物和内置态的准确性，直到可以验证或伪造时间变化的安全和不安全集给出的规格为止。数值评估表明，我们的验证算法成功地验证或伪造了来自不同领域的基准，而无需手动调整。
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.
