Verification and safety assessment of neural network controlled systems (NNCSs) is an emerging challenge. To provide guarantees, verification tools must efficiently capture the interplay between the neural network and the physical system within the control loop. In this paper, a compositional approach focused on inclusion preserving long term symbolic dependency modeling is proposed for the analysis of NNCSs. First of all, the matrix structure of symbolic zonotopes is exploited to efficiently abstract the input/output mapping of the loop elements through (inclusion preserving) affine symbolic expressions, thus maintaining linear dependencies between interacting blocks. Then, two further extensions are studied. Firstly, symbolic polynotopes are used to abstract the loop elements behaviour by means of polynomial symbolic expressions and dependencies. Secondly, an original input partitioning algorithm takes advantage of symbol preservation to assess the sensitivity of the computed approximation to some input directions. The approach is evaluated via different numerical examples and benchmarks. A good trade-off between low conservatism and computational efficiency is obtained.

翻译：神经网络控制系统（NNCSs）的验证与安全性评估是一项新兴挑战。为提供保障性证明，验证工具必须高效捕捉控制回路中神经网络与物理系统间的相互作用。本文提出一种聚焦于保包含长时符号依赖建模的组合分析方法，用于NNCSs特性分析。首先，利用符号多面体区域的矩阵结构，通过保包含的仿射符号表达式高效抽象回路元件的输入输出映射，从而维持交互模块间的线性依赖关系。继而研究两项扩展：其一，采用多项式符号集通过多项式符号表达式与依赖关系抽象回路元件行为；其二，创新性地提出一种基于符号保留特性的输入分区算法，用于评估计算近似对特定输入方向的敏感度。通过多项数值实例与基准测试对该方法进行评估，结果表明其能在低保守性与计算效率之间取得良好平衡。