While reachability analysis is one of the most promising approaches for 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.

翻译：尽管可达性分析是动态系统形式化验证中最有前景的方法之一，但阻碍其更广泛应用的主要缺点在于需要手动调整时间步长等算法参数。当需要验证系统是否满足由信号时序逻辑公式描述的复杂规约时，手动调整尤为困难，因为可达集紧致性对规约满足性的影响对人类而言往往难以直观判断。针对这一问题，我们提出一种面向线性系统的全自动验证器，该工具可自动优化可达性分析的所有参数，直至能够证明或证伪系统对所有初始状态及不确定输入是否满足信号时序逻辑公式。通过将可达时序逻辑与依赖保持技术相结合，我们的验证器构建了一种模型检测方法，该方法在参数适当调整时其过近似误差趋近于零。虽为简化起见本文聚焦线性系统，但所提出的通用概念同样适用于非线性及混合系统。