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.
@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} }
Bibliographic record
Deposited version
Deposited version
arts.units.it
Archivio istituzionale della ricerca - Università di Trieste
link.springer.com
A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems
Introduction to Runtime Verification
Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications
Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC