Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.

翻译：现代信息物理系统（CPS）可由多种相互交互与通信的网络化组件与智能体构成。在空间分布式CPS的背景下，这些连接能够动态地依赖于各组件与智能体的空间配置。在此类场景中，对分布式组件进行鲁棒监控对于确保实现复杂行为及维持安全属性至关重要。为此，我们研究如何为时空可达与逃逸逻辑（STREL）定义自动机语义。STREL是一种专门设计用于表达和监控移动、空间分布式CPS时空需求的形式逻辑。具体而言，STREL在动态加权图上进行时空行为推理。尽管STREL已具备定义明确的定性与定量语义，本文提出了一种从STREL规约构造（加权）交替有限自动机的新方法，该方法能高效编码这些语义。此外，我们通过模拟无人机集群环境，展示了如何利用此自动机语义对STREL规约同时执行离线与在线监控。