Despite the possibility to quickly compute reachable sets of large-scale linear systems, current methods are not yet widely applied by practitioners. The main reason for this is probably that current approaches are not push-button-capable and still require to manually set crucial parameters, such as time step sizes and the accuracy of the used set representation -- these settings require expert knowledge. We present a generic framework to automatically find near-optimal parameters for reachability analysis of linear systems given a user-defined accuracy. To limit the computational overhead as much as possible, our methods tune all relevant parameters during runtime. We evaluate our approach on benchmarks from the ARCH competition as well as on random examples. Our results show that our new framework verifies the selected benchmarks faster than manually-tuned parameters and is an order of magnitude faster compared to genetic algorithms.

翻译：尽管快速计算大规模线性系统可达集已成为可能，但现有方法尚未被实践者广泛采用。主要原因在于当前方法缺乏一键式操作能力，仍需手动设置关键参数（如时间步长、集合表示的精度），这需要专家知识。我们提出通用框架，能够在用户指定精度条件下自动为线性系统可达性分析寻找近优参数。为最大限度降低计算开销，我们的方法在运行时动态调优所有相关参数。我们在ARCH竞赛基准测试和随机示例上评估了该方法。结果表明，新框架验证选定基准测试的速度优于手动调优参数，且比遗传算法快一个数量级。