Summary: | 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.
|