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
@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} }