基于模型预测的动态系统在线监测方法，用于满足嵌套信号时序逻辑规范

《Nonlinear Analysis: Hybrid Systems》：Model predictive online monitoring of dynamical systems for nested signal temporal logic specifications

　　摘要：本文研究了在信号时态逻辑规范下，对网络物理系统进行在线监控的问题。其目标是设计一种在线监控器，该监控器能够基于截至当前时间的部分信号观测结果，在运行时评估系统的正确性，从而在规范被违反或未来必然会被违反时发出警报。我们考虑了一种模型预测式环境，其中系统的动态模型是可用的，并且可以被用来提高监控的准确性。然而，现有的方法仅限于一类受限的STL公式，只允许应用一次时态运算符。本文解决了在模型预测式监控器设计中处理嵌套时态运算符的挑战。我们的方法利用语法树结构来解决时态运算符之间的依赖关系，并引入了基本满足向量的概念。通过在线递归更新这些向量，同时结合从离线模型分析中得到的预计算满足区域，我们提出了一种新的模型预测式监控算法。我们证明了所提出的方法既可靠又完备，能够确保不会产生误报或漏报。文中还提供了案例研究以证明该方法的有效性。

引言：基于规范的监控已成为评估复杂工程网络物理系统安全性和正确性的常用方法，这类系统包括智慧城市[1]、自动驾驶车辆[2]以及工业物联网[3]。在这种背景下，监控器会观察系统生成的状态轨迹，并根据给定的正式规范来评估该轨迹的正确性[4]、[5]、[6]。与模型检验等形式化验证技术相比，监控的优势在于它更为轻量，因为它只需评估沿单一观测轨迹的系统正确性，而无需明确枚举所有可达状态空间。因此，监控可以独立设计，并作为附加模块应用于任意系统——甚至是那些被视为黑箱的系统。近年来，针对各种类型的正式规范，如线性时态逻辑[LTL][7]、度量时态逻辑[MTL][8]、[9]以及信号时态逻辑[STL][10]、[11]，在监控算法的设计方面取得了显著进展。在这些规范中，STL因其能够描述实值实时物理信号中的复杂时空约束，而成为CPS中最常用的正式规范之一。根据监控器可获取的信息不同，监控算法可进一步分为离线监控[9]、[12]和在线监控[8]、[10]。在离线环境中，监控器使用整个轨迹来评估系统的正确性。然而，这种方法不适用于实时运行的系统，因为这类系统只能获取到截至当前时刻的信号。相比之下，在线监控算法必须考虑到所有可能的未来行为，以便在规范被违反之前发出早期警告或终止相关进程。正因如此，在安全关键系统中，在线监控被广泛用作确保运营安全的预测性附加组件。由于系统的物理特性，在线信号通常并非随意产生，而是遵循一定的规则。通过利用有关系统行为的信息，我们可以更好地判断未来信号的可行性或可能性，从而做出更精确的监控决策[13]。为此，针对那些拥有明确模型或大量运行历史数据的系统，最近出现了预测性监控技术。例如，在[14]、[15]、[16]、[17]中，利用历史数据训练的神经网络被用来预测未来信号，以提高监控的准确性。然而，由于这些方法采用数据驱动的方式，其预测结果可能不可靠。为了解决这个问题，人们常常采用一致性预测等不确定性量化技术来确保预测的可靠性[18]、[19]、[20]。尽管这些方法有效，但可能会在最终的监控结果中引入额外的保守性。最近，通过利用底层动态系统的明确模型，人们在[21]中提出了一种名为模型预测监控的新框架。当拥有精确的系统模型时，这种方法能进一步提高监控的准确性。它通过将离线可达性计算与在线满足度评估相结合，实现了计算复杂度与准确度之间的有效平衡。在[22]中，为了降低状态采样开销，模型预测监控引入了一种自我触发的信息获取机制。然而，现有的模型预测监控算法仍然仅限于STL规范的简单片段，而且目前还不支持嵌套时态运算符，例如“最终始终处于某个区域”这样的表达。在本研究中，我们探讨了针对信号时态逻辑规范的模型预测式在线监控器的设计。与现有方法不同，我们考虑的是允许嵌套时态运算符的通用STL片段。这种嵌套结构带来了超出以往工作的新挑战，因为以往的工作是使用剩余公式的索引集来跟踪STL公式的进展。然而，由于运算符之间的依赖关系，这种方法在面对嵌套时态约束时会失效。为了解决这个问题，我们提议使用语法树[23]、[24]、[25]来解决时态运算符之间的依赖问题，并在在线监控过程中使用作为动态更新的关键信息的基本满足向量。我们的算法利用这些实时递归更新的向量，以及从离线模型分析中得到的预计算安全区域。这一框架成功地将模型预测监控扩展到了通用的STL规范。文中还提供了案例研究以证明该方法的有效性。

章节节选：系统模型：我们考虑一个离散时间控制系统，其形式为xk+1=f(xk,uk)，其中xk∈X?Rn表示时间点k∈Z≥0时的系统状态，uk∈U?Rm表示时间点k时的控制输入，f:X×U→X则是系统的动态函数，假定在X×U上连续。由于物理限制，我们假设状态空间X和输入空间U都是有界的。假设在时间点k时系统状态为xk。那么，给定一系列控制输入uk：T?1=ukuk+1…uT?1∈UT?k，相应的STL公式片段：在本文中，我们考虑以下略有限制的STL公式片段：?φ??∣πμ∣?φ∣φ1∧φ2 ?Φ?F[a,b]Φ∣G[a,b]Φ∣Φ1U[a,b]Φ2∣Φ1∧Φ2∣φ。与完整的STL片段相比，我们要求否定操作只能应用于布尔运算符。因此，所考虑的整个STL公式是一组子公式的合取，其中的嵌套时态运算符可以应用于任意的布尔公式。出于技术上的考虑，我们引入了一个新的时态运算符U′，其定义为：(x,k)。嵌套STL公式树：处理包含嵌套时态运算符的STL公式的主要挑战在于内部运算符和外部运算符之间的依赖关系。例如，考虑STL公式G[a1,b1]F[a2,b2]φ。这个公式要求在a1和b1之间的所有时间点上，内部的公式F[a2,b2]φ都必须得到满足。具体来说，从[a1,b1]区间内的任意时间点开始，系统应在该时间点之后的[a2,b2]区间内满足φ条件。因此，要评估系统的正确性，就需要……基本向量的演变：为了在不存储整个状态轨迹的情况下跟踪STL公式的进展，我们的方法是仅维护基本满足向量，并在每个时间点观察到新的系统状态时递归地更新它们。这种递归计算的过程如下：•初始化：在时间点k=0时，即在观察到任何系统状态之前，初始的基本向量集被定义为：I0=(?0v1,?0v2,…,?0vh)，其中每个?0vi=(?,?,…,?)是一个所有元素都被初始化为……在线监控的案例研究：在本节中，我们通过两个案例来说明我们的在线监控算法。我们是用Python语言实现上述方法的。1结论：在本文中，我们提出了一种基于模型的在线监控算法，用于处理带有嵌套时态逻辑的STL公式，该算法利用语法树结构，通过简单的向量更新实现了高效的在线执行，不过对于具有复杂动态特性的系统，离线可行集的计算仍然是一项艰巨的任务。在未来的工作中，我们计划从三个方向扩展这一框架：（1）通过整合概率可达性来输出满足概率，从而处理随机系统；（2）通过……CRediT作者贡献声明：韩涛：形式化分析、概念构建。李少远：监督、形式化分析。尹翔：监督、形式化分析、概念构建。利益冲突声明：作者们声明存在以下可能被视为潜在利益冲突的财务利益/个人关系：尹翔表示获得了中国国家自然科学基金的财政支持。尹翔还表明与中国国家自然科学基金之间存在包括资金资助在内的关系。如果有其他作者，他们声明自己没有已知的可能被视为利益冲突的财务利益或个人关系。韩涛|李少远|尹翔中国上海交通大学自动化与智能感知学院，上海200240