一句话：提出信号时空逻辑 SSTL 及其布尔与定量监控算法，用于时空系统的实时验证。
面向智慧城市与信息物理系统等空间分布的大规模系统，时间与空间动态相互交织并驱动系统行为。本文提出信号时空逻辑 SSTL，一种用于规约线性时间与离散空间模型的模态逻辑。SSTL 将 until 时间模态与两个空间模态相结合：一个表达“附近某处为真”，另一个表达“被满足给定时空性质的区域所包围”。该逻辑同时具有布尔语义与定量语义，作者为其开发了高效监控算法，可用于白盒与黑盒复杂系统的实时验证，并可与随机模型检测例程组合。监控算法已实现于开源 Java 工具中。文章通过图灵反应扩散系统中的模式形成以及大型共享单车系统的时空性质分析，展示了 SSTL 的实用性与表达能力。
In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which efficient monitoring algorithms have been developed. As such, it is suitable for real-time verification of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satisfies a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diffusion system and spatio-temporal aspects of a large bike-sharing system. Comment: 36 pages with 13 figures
@article{paperbot369,
title = {Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL},
author = {L. Nenzi and L. Bortolussi and V. Ciancia and M. Loreti and M. Massink},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
number = {Modal and temporal logics},
year = {2018},
doi = {10.23638/lmcs-14(4:2)2018}
}