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 ecient monitoring algorithms have been developed. As such, it is suitable for real-time verication 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 satises 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-Diusion system and spatio-temporal aspects of a large bike-sharing system.

Qualitative and quantitative monitoring of spatio-temporal properties with SSTL

Ciancia V;Massink M
2018

Abstract

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 ecient monitoring algorithms have been developed. As such, it is suitable for real-time verication 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 satises 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-Diusion system and spatio-temporal aspects of a large bike-sharing system.
2018
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
Spatio-Temporal Logic
Signal Temporal Logic
Quantitative Semantics
Monitoring Algorithms
Real-Time Verification
Turing Pattern
Bike Sharing
Statistical Model Checking
File in questo prodotto:
File Dimensione Formato  
prod_393208-doc_135983.pdf

accesso aperto

Descrizione: Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
Tipologia: Versione Editoriale (PDF)
Dimensione 2.07 MB
Formato Adobe PDF
2.07 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/344862
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 37
  • ???jsp.display-item.citation.isi??? 28
social impact