论文标题
通过模型信息的在线监视动态系统，以进行信号时间逻辑规格
Online Monitoring of Dynamic Systems for Signal Temporal Logic Specifications with Model Information
论文作者
论文摘要
在线监视旨在评估或预测系统的行为是否满足某些所需规范。它在安全至关重要的网络物理系统中起关键作用。在这项工作中，我们提出了一种基于模型的新方法，用于在线监视信号时间逻辑（STL）公式所描述的规格。具体而言，我们假设观察到的状态痕迹是由已知模型的基础动态系统生成的。主要思想是在评估STL公式的满意度时考虑系统的动态。为此，提供了用于计算STL公式的可行集合的有效方法。我们表明，通过明确利用动态系统的模型信息，与现有算法相比，所提出的在线监视算法可以预先伪造或证明该规范的规范，而该算法没有使用模型信息。我们还通过案例研究证明了所提出的监测算法。
Online monitoring aims to evaluate or to predict, at runtime, whether or not the behaviors of a system satisfy some desired specification. It plays a key role in safety-critical cyber-physical systems. In this work, we propose a new model-based approach for online monitoring for specifications described by Signal Temporal Logic (STL) formulae. Specifically, we assume that the observed state traces are generated by an underlying dynamic system whose model is known. The main idea is to consider the dynamic of the system when evaluating the satisfaction of the STL formulae. To this end, effective approaches for the computation of feasible sets for STL formulae are provided. We show that, by explicitly utilizing the model information of the dynamic system, the proposed online monitoring algorithm can falsify or certify of the specification in advance compared with existing algorithms, where no model information is used. We also demonstrate the proposed monitoring algorithm by case studies.
