PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M. Qualitative and quantitative monitoring of spatio-temporal properties. In: RV 2015 - Runtime Verification 2015. 6th International Conference (Vienna, Austria, 22 - 25 September 2015). Proceedings, pp. 21 - 37. Ezio Bartocci, Rupak Majumdar (eds.). (Lecture Notes in Computer Science, vol. 9333). Springer, 2015.
 
 
Abstract
(English)
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.
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-23820-3_2
DOI: 10.1007/978-3-319-23820-3_2
Subject Modal Logics
Model Checking
Spatial Logic
F.4.1 Mathematical Logic
D.2.4 Software/Program Verification. Model checking


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional