Qualitative and quantitative monitoring of spatio-temporal properties
Posted by luca | On Wednesday, 27 January 2016
Title | Qualitative and quantitative monitoring of spatio-temporal properties |
Publication Type | Conference Paper |
Year of Publication | 2015 |
Authors | Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M |
Conference Name | Runtime Verification (RV) |
Volume | 9333 |
Series | LNCS |
Pages | 21–37 |
Publisher | Springer International Publishing |
Keywords | Boolean semantics, Monitoring algorithms, Quantitative semantics, Signal spatio-temporal logic, Turing patterns, Weighted graphs |
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. |
DOI | 10.1007/978-3-319-23820-3_2 |
File: