Qualitative and Quantitative Monitoring of Spatio-Temporal Properties

Abstract. We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.

• Type: Journal
• Year: 2015
• Where: RV
• Authors: Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, Mieke Massink
• Keywords: Hardware, RV 2015