From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires to reason about complex spatio-temporal properties of physical and/or computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and to reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing their spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.

翻译：从生物系统到网络物理系统,监测这些动态系统的行为往往需要了解动态相互联系并在特定空间配置中安排的物理和(或)计算实体的复杂时空特性。Spatio-Temoal Areating and Escape Locic(STREL)是最近一种基于逻辑的正式语言,旨在说明和解释spatio-时间特性。STREL认为每个系统实体是代表其空间安排的动态加权图表的节点。每个节点产生一组混合分析信号,描述显示显示该节点行为在计算和物理数量方面的演变过程。虽然有非在线算法可用于监测STREL对登录模拟痕迹的规格,但在这里我们首次调查一种在线算法,使系统执行或模拟期间的运行时间核查能够进行。我们的方法通过考虑不精确的信号和增强逻辑的语义来扩展最初的框架,从而有可能表达系统行为是否符合其规格的部分保证。最后,我们在现实世界环境监测案例研究中展示了我们的方法。