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. Extended version. QUANTICOL Technical Report. Technical report, 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. Keywords: Signal Spatio-Temporal Logic, Boolean Semantics, Quantitative Semantics, Monitoring Algorithms, Weighted Graphs, Turing Patterns.
Subject Spatial Logics
F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs
03B70 Logic in computer science


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