While reachability analysis is one of the most promising approaches for the formal verification of dynamic systems, a major disadvantage preventing a more widespread application is the requirement to manually tune algorithm parameters such as the time step size. Manual tuning is especially problematic if one aims to verify that the system satisfies complicated specifications described by signal temporal logic formulas since the effect the tightness of the reachable set has on the satisfaction of the specification is often non-trivial to see for humans. We address this problem with a fully-automated verifier for linear systems, which automatically refines all parameters for reachability analysis until it can either prove or disprove that the system satisfies a signal temporal logic formula for all initial states and all uncertain inputs. Our verifier combines reachset temporal logic with dependency preservation to obtain a model checking approach whose over-approximation error converges to zero for adequately tuned parameters. While we in this work focus on linear systems for simplicity, the general concept we present can equivalently be applied for nonlinear and hybrid systems.

翻译：可达性分析是动态系统形式化验证最具前景的方法之一，但其手动调节算法参数（如时间步长）的要求限制了更广泛的应用。当需要验证系统满足由信号时态逻辑公式描述的复杂规范时，手动调参尤为棘手，因为可达集紧致性对规范满足性的影响对人类而言往往难以直观判断。针对线性系统，我们提出一种全自动验证器，可自动细化可达性分析的所有参数，直至能够证明或证伪系统对所有初始状态及所有不确定性输入满足信号时态逻辑公式。该验证器通过结合可达集时态逻辑与依赖保持方法，构建了一种过逼近误差可在参数充分调优时收敛至零的模型检验方案。虽然本文为简便起见聚焦于线性系统，但所提出的通用概念同样适用于非线性系统与混合系统。