一种用于监测空间分布式信息物理系统动态网络的逻辑
计算机科学中的逻辑
2023-06-22 v4
摘要
信息物理系统（CPS）由通过传感器和/或执行器交互的紧密交织的计算（赛博）与物理组件构成。计算元素在各尺度上组网，并可彼此通信以及与人类通信。节点可随时加入和离开网络，或移动到不同的空间位置。在此情形下，监测空间与时间性质对于理解复杂行为如何由局部与动态交互涌现起着关键作用。我们在此重新审视时空可达与逃逸逻辑（STREL），这是一种基于逻辑的形式化语言，旨在表达并监测移动与空间分布式 CPS 执行过程中的时空需求。STREL 将 CPS 实体（图节点）所处的物理空间视为表示其动态拓扑配置的加权图。节点与边均包含建模可随时间演化的物理与逻辑量的属性。STREL 将信号时序逻辑与在加权图上运作的两个空间模态 reach 与 escape 结合。由这些基本算子可派生出其他重要的空间模态，如 everywhere、somewhere 与 surround。我们基于约束半环代数结构提出定性与定量语义。我们给出 STREL 的离线监测算法，并通过两个案例研究展示方法的可行性：对模拟移动自组织传感器网络的时空需求监测，以及对 COVID19 的模拟疫情传播模型。
引用
@article{arxiv.2105.11400,
title = {A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems},
author = {L. Nenzi and E. Bartocci and L. Bortolussi and M. Loreti},
journal= {arXiv preprint arXiv:2105.11400},
year = {2023}
}
备注
arXiv admin note: substantial text overlap with arXiv:1904.08847