Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL). The classic STL monitoring is performed by computing a robustness interval that specifies, at each instant, how far the monitored signals are from violating and satisfying the specification. However, since a robustness interval monotonically shrinks during monitoring, classic online monitors may fail in reporting new violations or in precisely describing the system evolution at the current instant. In this paper, we tackle these issues by considering the causation of violation or satisfaction, instead of directly using the robustness. We first introduce a Boolean causation monitor that decides whether each instant is relevant to the violation or satisfaction of the specification. We then extend this monitor to a quantitative causation monitor that tells how far an instant is from being relevant to the violation or satisfaction. We further show that classic monitors can be derived from our proposed ones. Experimental results show that the two proposed monitors are able to provide more detailed information about system evolution, without requiring a significantly higher monitoring cost.
翻译:在线监测是混合系统的一种有效验证方法,它能在运行时检查系统的(部分)信号是否满足某种规范(例如信号时序逻辑规范)。经典的STL监测通过计算鲁棒性区间来执行,该区间在每个时刻指示被监测信号距离违反和满足规范的程度。然而,由于鲁棒性区间在监测过程中单调收缩,经典的在线监测器可能无法报告新的违规情况,也无法精确描述当前时刻的系统演化。本文通过考虑违规或满足的因果关系(而非直接使用鲁棒性)来解决这些问题。我们首先引入一个布尔因果关系监测器,用于判定每个时刻是否与规范违规或满足相关。随后将该监测器扩展为定量因果关系监测器,用于量化每个时刻与规范违规或满足的相关程度。进一步证明经典监测器可由本文提出的监测器推导得出。实验结果表明,所提出的两种监测器能够在不显著增加监测成本的情况下,提供更详细的系统演化信息。