Document - Qualitative and quantitative monitoring of spatio-temporal properties

2015

Conference article Open Access

Qualitative and quantitative monitoring of spatio-temporal properties

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

Weighted graphs Spatial Logic Turing patterns Computer Science (all) Boolean semantics Software/Program Verification. Model checking Modal Logics Model Checking Quantitative semantics Theoretical Computer Science Mathematical Logic Signal spatio-temporal logic Monitoring algorithms

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.

Citations

Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors. Handbook of Spatial Logics. Springer, 2007.
E. Bartocci, L. Bortolussi, L. Nenzi, and G. Sanguinetti. System design of stochastic models using robustness of temporal properties. Theoretical Computer Science, 2015.
L. Bortolussi and L. Nenzi. Specifying and monitoring properties of stochastic spatiotemporal systems in signal temporal logic. In Proceedings of VALUETOOLS, 2014.
V. Ciancia, D. Latella, M. Loreti, and M. Massink. Specifying and verifying properties of space. In Proceedings of IFIP-TCS, number 8705 in LNCS, pages 222-235, 2014.
Vincenzo Ciancia, Stephen Gilmore, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. Spatio-temporal model-checking of vehicular movement in public transport systems. Submitted, 2015.
Vincenzo Ciancia, Stephen Gilmore, Diego Latella, Michele Loreti, and Mieke Massink. Data verification for collective adaptive systems: Spatial model-checking of vehicle location data. In Proceedings of SASOW, 2014.
A. Donze´, T. Ferrer, and O. Maler. Efficient robust monitoring for stl. In Proc. of CAV'13, volume 8044 of LNCS, pages 264-279, 2013.
A. Donze´ and O. Maler. Robust satisfaction of temporal logic over real-valued signals. In Proc. of FORMATS, volume 6246, pages 92-106, 2010.
Georgios E. Fainekos and George J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42):4262-4291, September 2009.
Antony Galton. The mereotopology of discrete space. In Christian Freksa and DavidM. Mark, editors, Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science, volume 1661 of Lecture Notes in Computer Science, pages 251-266. Springer Berlin Heidelberg, 1999.
E. Aydin Gol, E. Bartocci, and C. Belta. A formal methods approach to pattern synthesis in reaction diffusion systems. In Proceedings of CDC, 2014.
R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. A. Smolka, and A. Wasilewska. Learning and detecting emergent behavior in networks of cardiac myocytes. In Proceedings of HSCC'08, pages 229-243, 2008.
I. Haghighi, A. Jones, J. Z. Kong, E. Bartocci, Grosu R., and C. Belta. SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems. In Proceedings of HSCC, 2015.
O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Proceedings FORMATS 2004, volume 3253, pages 152-166, 2004.
L. Mari, E. Bertuzzo, L. Righetto, R. Casagrandi, M. Gatto, I. Rodriguez-Iturbe, and A. Rinaldo. Modelling cholera epidemics: the role of waterways, human mobility and sanitation. Journal of The Royal Society Interface, 9(67):376-388, February 2012.
A. M. Turing. The Chemical Basis of Morphogenesis. Philosophical Transactions of the Royal Society of London B: Biological Sciences, 237(641):37-72, August 1952.

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:334872,
	title = {Qualitative and quantitative monitoring of spatio-temporal properties},
	author = {Nenzi L and Bortolussi L and Ciancia V and Loreti M and Massink M},
	doi = {10.1007/978-3-319-23820-3_2},
	year = {2015}
}