Document - Qualitative and quantitative monitoring of spatio-temporal properties. Extended version

2015

Report Open Access

Qualitative and quantitative monitoring of spatio-temporal properties. Extended version

Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.

Spatial logics Specifying and verifying and reasoning about programs

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.

Source: ISTI Technical reports, 2015

Back to previous page

Cite as

BibTeX entry

@techreport{oai:it.cnr:prodotti:362790,
	title = {Qualitative and quantitative monitoring of spatio-temporal properties. Extended version},
	author = {Nenzi L. and Bortolussi L. and Ciancia V. and Loreti M. and Massink M.},
	institution = {ISTI Technical reports, 2015},
	year = {2015}
}