《自主系统的组成分析》美空军2022最新报告

网络物理系统（CPS）由相互作用的计算和物理组件组成。该项目旨在开发创新的验证技术以保证网络物理系统的安全行为。混合系统[5]是一个富有表现力的数学模型，有助于描述涉及连续和离散状态及其演变的复杂动态过程，这使得它们特别适合于为CPS建模。在这个项目中，我们专注于开发混合系统可达性分析的新技术，即自动探索给定动态系统的状态空间并计算系统轨迹的包络，给定其不确定参数的边界的技术。为了减轻系统的复杂性，我们的目标是发展组合方法，即把系统分析分解为各部分的分析方法。考虑到这一总体目标，我们在这个项目中的活动可以大致分为以下几个研究方向：

以线性微分方程为特征的系统的可达性方法。虽然现代线性代数软件包对数万维的矩阵是有效的，但基于集合的图像计算却仅限于几百维。在[9]中，我们提出了分解到达集的计算，使集的操作在低维度上进行，而像指数化这样的矩阵操作则在全维度上进行。我们的方法适用于密集型和离散型的设置。对于一组标准的基准，它显示出与各自的最先进的工具相比，速度提高了两个数量级，而在精度上只有少量的损失。对于密集时间的情况，我们展示了一个超过10,000个变量的实验，大约比以前的方法高两个数量级。这些算法为JuliaReach[10]奠定了基础，JuliaReach是一个用于基于集合的动态系统可达性分析的工具箱。JuliaReach由两个主要包组成。Reachability，包含连续和混合系统的可达性算法的实现，以及LazySets，一个独立的库，实现最先进的凸集计算算法。该库同时提供了具体的和懒惰的集合表示，后者代表了将集合计算延迟到需要时才进行的能力。我们扩展了[8]中的这些结果，增加了对任意大小分区和任意低维集合表示的支持。在一个相关的工作中[11]，我们沿着复杂度的不同维度扩展了这些结果，即提出了一种有效处理混合系统离散转换的组合方式。

伪造方法。混合系统的证伪是与验证相对应的，目的是找到违反给定安全属性的轨迹。这是一个具有挑战性的问题，目前伪造算法的实际适用性仍然受制于其高时间复杂性。在[13]中，我们试图利用我们已经开发的可达性算法的力量来提高伪造技术的可扩展性。特别是，我们从现有的伪造问题的编码作为一个非线性优化问题开始[25]，并提出了一个扩展，通过增加用可达性算法获得的线性状态约束来减少优化问题的搜索空间。我们在一些标准的混合系统基准上展示了我们方法的效率，证明了在速度和可伪造实例数量上的性能提升。在[12]中，我们通过将非线性优化问题分解为两个更简单的优化问题，并以交替的方式解决它们来增强这种算法。

并行方法。如上所述，可达性分析技术是目前验证网络物理系统安全属性的最先进技术的核心。在这个主旨中，我们研究了如何利用现代CPU中强大的并行多核架构来扩展此类技术。在文献[18]中，我们首次提出了一套并行状态空间探索算法，利用多核CPU，能够对CPS的线性连续和混合自动机模型进行可达性分析，从而解决了这一限制。为了证明在多核处理器上实现的性能加速，我们在几个基准上对所提出的并行算法进行了实证评估，比较其关键性能指标。

库普曼算子理论。非线性动力系统的可达性分析是一项具有挑战性和计算成本的任务。同时，如上所述，计算线性系统的可达状态，通常可以在高维度上有效地完成。在[6]中，我们探讨了利用这两类系统之间的联系的验证方法，该方法基于Koopman算子的概念[23]。Koopman算子将非线性系统的行为与嵌入高维空间的线性系统联系在一起，并增加了一组所谓的可观察变量。尽管新的动态系统有线性微分方程，但初始状态集是用非线性约束条件定义的。由于这个原因，现有的线性系统可达性方法不能直接使用。我们提出了第一个可达性算法，以处理这种未曾探索过的可达性问题的类型。我们的评估考察了几种优化方法，并表明所提出的工作流程是验证非线性系统行为的一个很有前途的途径。

可达性分析的混合方法。这些方法[7]通过用较简单的动力学（如常数或仿生动力学）来近似非线性动力学。这一步使我们有可能利用现有的线性动力学混合系统的算法的力量。在[20]中，我们提出了基于动力学比例模型转换的混合方法的改进。该转换旨在减少线性化域的大小，从而减少超近似误差。我们在一些非线性基准实例上展示了我们方法的效率。

在线验证。在这个研究方向中，我们的目标是将可达性分析应用于在线环境中。换句话说，我们考虑的环境是，可达性分析所提供的信息被实时用于指导自主系统的控制算法。这反过来又对可达性分析的性能效率提出了特别严格的时间限制。在[14]中，我们提出了一种方法，利用深度神经网络在有限的时间内对可达集进行保守的近似。我们提供了基于统计模型检查方法的概率性保证。该方法被评估为自主车辆在模拟环境中几个动作的弹性安全架构的一部分。我们的评估表明，可达性分析可以在几分之一秒内完成，并且比传统的非线性可达性工具要好两个数量级。我们还提出了另一种方法[1]，通过将障碍证书[22]的计算泛化到动态变化的初始条件，以及在运行时使用生成的安全集来对抗先前未知的、可能与时间有关的不安全集，从而有效地进行实时可达性分析。这些方法得到了[15]的补充，在那里我们探讨了如何将可达性分析作为模型预测控制[17]的一部分来支持动态避障。

通过验证进行规划。在我们的早期工作[16]中，我们通过提供从PDDL+（一种描述规划领域的形式主义）到混合系统的转换方案，在弥合混合自动机的规划和验证领域之间的差距方面迈出了第一步。这使得模型检验工具能够在混合规划领域得到应用。通过这种方式，我们可以解决最先进规划器范围之外的PDDL+领域。在这个项目中，我们将[19]中的这些想法改编为时态规划，并将我们的方法纳入到细化循环中。我们还提出了一个基于抽象的放松[21]，用于推理线性数字规划问题。

混合系统的Event-B。在这个研究方向上，我们考虑了Event-B[2]和混合系统之间的协同作用。我们在这一领域的成果包括开发了一个通用的混合铁路信号系统模型[3]，该模型可以进一步完善，以捕捉特定的铁路信号系统。另外，在[4]中，我们提出了一种网络物理系统的多元开发方法，该方法建立在基于细化和证明的建模语言Event-B及其对混合系统建模的扩展。为了提高该方法中所产生的Event-B模型的低演绎验证自动化程度，这项工作描述了一种在证明过程中整合可达性分析的新方法。此外，为了提供更全面的网络物理系统开发和基于仿真的验证，我们描述了将网络物理系统Event-B模型转化为Simulink的机制。

随机常微分方程（RODEs）。顾名思义，这些是在其向量场函数中包含随机过程的常微分方程（ODEs）。它们已经在广泛的应用中使用了很多年，但一直是随机微分方程（SDEs）的影子存在，尽管能够对更广泛的、通常在物理上更充分的干扰进行建模。在[24]中，我们研究了包含维纳过程的RODEs在有限时间跨度和无限时间跨度上的安全验证问题。更详细地说，我们研究了p-安全问题，其中我们确定了满足安全规范的概率至少为p的初始状态集。基于确定概率测量大于p的样本路径集，我们提出了一种将ODEs的随机可达性减少为对抗性可达性的方法，以解决有限时间范围内的p-安全问题。这种方法允许将扰动的ODEs的可达性计算方法有效地提升到RODEs。在这个方法中，有限时间范围内的p-安全问题被简化为具有时间变化的扰动输入的ODEs的内部逼近鲁棒的后向可达集问题。然后，我们将该方法扩展到无限时间跨度的p-安全问题。最后，我们在几个例子上演示了我们的方法。