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.

翻译：可达性分析是一种在不确定性影响下保证动态系统安全性的形式化方法。所有可达性算法的一个关键瓶颈是需要专家知识来充分调整特定算法参数（如时间步长）。本文通过提出一种全自动可达性算法解决了该问题，该算法内部自动调整所有算法参数，使得可达集包络在豪斯多夫距离意义下满足用户定义的近似误差界。此外，该误差界可用于通过闵可夫斯基差从外逼近中提取可达集的内逼近。最后，我们提出了一种新颖的验证算法，该算法自动细化外逼近和内逼近的精度，直至由时变安全集与不安全集给定的规约被验证或证伪。数值评估表明，本验证算法无需人工调参即可成功验证或证伪不同领域的基准案例。