AI 中文总结
针对无全局时钟的分布式CPS，研究人员提出首个算法，将STL扩展到部分同步时钟场景，可返回满足规范的全局时刻集合，实现有效监控，复杂度可推导，适用于最多50个智能体的场景。
AI 中文摘要
我们针对分布式网络物理系统（CPS）针对稠密时间时序逻辑规范的连续监控，给出了首个理论刻画和首个算法。分布式CPS由多个智能体组成，每个智能体都有一个本地时钟，这些时钟彼此漂移，因此不存在明确定义的全局时间。当针对时序逻辑规范监控此类系统的输出信号时，如何解释公式的时间约束以及满足的含义尚不明确。然而，CPS设计者（如控制工程师）通常从全局时间的角度考虑系统的运行。大多数现有的分布式系统监控技术适用于离散时间规范，不适用于CPS，且/或需要将时间约束显式映射到本地时钟。我们针对仍包含所有时序算子的信号时序逻辑（STL）片段，引入了一种解决上述挑战的算法。该算法依赖于将满足信号新颖扩展到这种部分同步设置（其中时钟漂移），并对多维部分同步时间的几何进行分析。该算法返回所有可能满足规范的全局时刻的集合。了解这些可能的全局时刻对于调试分布式混合控制系统（如无人机机群和电网）非常重要。我们推导了该算法的最坏情况复杂度，并实现了其可靠近似，实验表明即使在多达50个智能体的场景中也能实现有效监控。
英文摘要
We give the first theoretical characterization, and the first algorithm, for continuous monitoring of a distributed Cyber-Physical System (CPS) against a dense-time temporal logic specification. A distributed CPS is composed of multiple agents, each with a local clock; these clocks drift from each other, so there is no well-defined global time. When monitoring such a system's output signal against a temporal logic specification, it is not evident how to interpret the temporal constraints of the formula, and what satisfaction means. Yet CPS designers, like control engineers, typically think of their system's operation in terms of global time. Most existing techniques for monitoring distributed systems work with discrete-time specifications not suitable for CPS, and/or require an explicit mapping of temporal constraints to local clocks. We introduce an algorithm that addresses the above challenges for a fragment of Signal Temporal Logic (STL) that still includes all temporal operators. It relies on a novel extension of satisfaction signals to this partially synchronous setting (where clocks drift), and an analysis of the geometry of multi-dimensional partially synchronous time. The algorithm returns the set of all possible global moments that can satisfy the specification. Knowledge of these possible global moments is important for debugging distributed hybrid control systems such as fleets of drones and electrical grids. We derive the worst-case complexity of the algorithm, and implement a sound approximation of it that experimentally illustrates effective monitoring, even in scenarios of up to 50 agents.
CommentsAccepted to Runtime Verification 2026
