时空属性的定性和定量监测与SSTL
摘要：空间定位的大规模系统中，时间和空间动力学相互作用并驱动其行为。这种系统的例子可以在许多智能城市应用和物理系统中找到。在本文中，我们介绍了信号时空逻辑(SSTL)，这是一种可以用来指定线性时间和离散空间模型的时空属性的模态逻辑。该逻辑具有布尔和定量语义，且已开发出高效的监测算法。因此，它适用于白盒和黑盒复杂系统的实时验证。这些算法还可以与随机模型检测例程结合使用。SSTL将直到时间模态与两个空间模态相结合，一个表达在某个附近某事物为真，另一个捕捉到被满足某给定时空属性的区域包围。监测算法在一个开源的Java工具中实现。我们通过分析图灵反应扩散系统的模式形成和一个大型自行车共享系统的时空方面来说明SSTL的使用。
作者：L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, M. Massink
论文ID：1706.09334
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22