SSTL对时空属性的定性与定量监控
Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
AI总结：
本文提出信号时空逻辑（SSTL），用于指定和监控线性时间与离散空间模型的时空属性，支持布尔与定量语义，并应用于图灵反应-扩散系统和大型共享单车系统验证。
摘要：
在空间分布的大规模系统中，时间与空间的动态相互作用并驱动系统行为。此类系统的实例常见于众多智慧城市应用和网络物理系统中。本文提出了信号时空逻辑（SSTL），这是一种可用于指定线性时间和离散空间模型的时空属性的模态逻辑。该逻辑配备了布尔语义和定量语义，并已为其开发了高效的监控算法。因此，它适用于白盒和黑盒复杂系统的实时验证。这些算法还可与随机模型检验程序相结合。SSTL将“直到”时间模态与两种空间模态相结合，一种表达某事物在附近某处为真，另一种捕捉被满足给定时空属性的区域所包围的概念。监控算法已在一个开源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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
