We present the first decentralized algorithm for detecting predicates over continuous-time signals under partial synchrony. A distributed cyber-physical system (CPS) consists of a network of agents, each of which measures (or computes) a continuous-time signal. Examples include distributed industrial controllers connected over wireless networks and connected vehicles in traffic. The safety requirements of such CPS, expressed as logical predicates, must be monitored at runtime. This monitoring faces three challenges: first, every agent only knows its own signal, whereas the safety requirement is global and carries over multiple signals. Second, the agents' local clocks drift from each other, so they do not even agree on the time. Thus, it is not clear which signal values are actually synchronous to evaluate the safety predicate. Third, CPS signals are continuous-time so there are potentially uncountably many safety violations to be reported. In this paper, we present the first decentralized algorithm for detecting conjunctive predicates in this setup. Our algorithm returns all possible violations of the predicate, which is important for eliminating bugs from distributed systems regardless of actual clock drift. We prove that this detection algorithm is in the same complexity class as the detector for discrete systems. We implement our detector and validate it experimentally.
翻译:摘要:我们提出了首个在部分同步条件下对连续时间信号进行谓词检测的去中心化算法。分布式信息物理系统由多个智能体组成,每个智能体测量(或计算)一个连续时间信号,例如通过无线网络连接的分布式工业控制器或交通中的网联车辆。此类系统的安全需求(以逻辑谓词形式表达)需在运行时进行监控。该监控面临三个挑战:首先,每个智能体仅知晓自身信号,而安全需求是全局性的且涉及多个信号;其次,智能体的本地时钟相互漂移,因此它们甚至无法在时间上达成一致,从而无法明确哪些信号值真正同步以评估安全谓词;第三,信息物理系统的信号是连续时间的,因此可能存在不可数多个需要报告的安全违规。本文提出了首个在此场景下检测合取谓词的去中心化算法,该算法返回所有可能的谓词违规,这对于消除分布式系统中与实际时钟漂移无关的缺陷至关重要。我们证明了该检测算法与离散系统检测器属于同一复杂度类别,并通过实验验证了其性能。