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.
Titolo: | Qualitative and quantitative monitoring of spatio-temporal properties |
Autori: | |
Data di pubblicazione: | 2015 |
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. |
Handle: | http://hdl.handle.net/11368/2856192 |
ISBN: | 9783319238197 |
URL: | http://springerlink.com/content/0302-9743/copyright/2005/ |
Appare nelle tipologie: | 4.1 Contributo in Atti Convegno (Proceeding) |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
RV15-post.pdf | Post-print | Bozza finale post-referaggio (post-print) | Digital Rights Management non definito | Open Access Visualizza/Apri |
RV2015-1.pdf | Documento in Versione Editoriale | Copyright Editore | Administrator Richiedi una copia |