Qualitative and quantitative monitoring of spatio-temporal properties

TitleQualitative and quantitative monitoring of spatio-temporal properties
Publication TypeConference Paper
Year of Publication2015
AuthorsNenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M
Conference NameRuntime Verification (RV)
PublisherSpringer International Publishing
KeywordsBoolean semantics, Monitoring algorithms, Quantitative semantics, Signal spatio-temporal logic, Turing patterns, Weighted graphs

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.