Reachability analysis is a powerful tool for computing the set of states or outputs reachable for a system. While previous work has focused on systems described by state-space models, we present the first methods to compute reachable sets of ARMAX models - one of the most common input-output models originating from data-driven system identification. The first approach we propose can only be used with dependency-preserving set representations such as symbolic zonotopes, while the second one is valid for arbitrary set representations but relies on a reformulation of the ARMAX model. By analyzing the computational complexities, we show that both approaches scale quadratically with respect to the time horizon of the reachability problem when using symbolic zonotopes. To reduce the computational complexity, we propose a third approach that scales linearly with respect to the time horizon when using set representations that are closed under Minkowski addition and linear transformation and that satisfy that the computational complexity of the Minkowski sum is independent of the representation size of the operands. Our numerical experiments demonstrate that the reachable sets of ARMAX models are tighter than the reachable sets of equivalent state space models in case of unknown initial states. Therefore, this methodology has the potential to significantly reduce the conservatism of various verification techniques.
翻译:可达性分析是一种计算系统可达状态或输出集合的强大工具。尽管先前的研究聚焦于状态空间模型描述的系统,但我们首次提出了计算ARMAX模型(数据驱动系统辨识中最常见的输入-输出模型之一)可达集的方法。我们提出的第一种方法仅适用于依赖保持的集合表示(如符号多面体),而第二种方法对任意集合表示均有效,但需基于ARMAX模型的重构。通过计算复杂度分析表明,当使用符号多面体时,两种方法相对于可达性问题的时域均呈二次方扩展。为降低计算复杂度,我们提出第三种方法,该方法在集合表示对闵可夫斯基加法和线性变换封闭,且闵可夫斯基和的计算复杂度独立于操作数表示大小时,相对于时域呈线性扩展。数值实验表明,在初始状态未知的情况下,ARMAX模型的可达集比等效状态空间模型的可达集更紧凑。因此,该方法有望显著降低各类验证技术的保守性。