面向信号时序逻辑规范的动态系统模型预测监控

在线监控旨在在运行时评估或预测系统的行为是否满足某些期望的规范。它在安全关键的信息物理系统中起着关键作用。在这项工作中，我们提出了一种称为模型预测监控的新监控方法，用于由信号时序逻辑（Signal Temporal Logic, STL）公式描述的规范。具体而言，我们假设观测到的状态轨迹由一个底层动态系统生成，该系统的模型已知但控制律未知。主要思想是在评估 STL 公式的满足性时使用系统的动态来预测未来状态。为此，提供了用于计算 STL 公式可行集的有效方法。我们表明，通过显式利用动态系统的模型信息，所提出的在线监控算法相比现有未使用模型信息的算法能够提前证伪或验证规范。我们还通过几个真实世界的案例研究演示了所提出的监控算法。