Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
Title | Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic |
Publication Type | Conference Paper |
Year of Publication | 2015 |
Authors | Bortolussi L, Nenzi L |
Conference Name | VALUETOOLS2014 |
Volume | 1 |
Series | EAI ENDORSED TRANSACTIONS ON CLOUD SYSTEMS |
Issue | 4 |
Keywords | Monitoring, Signal Temporal Logic, Spatial Logic, Spatio-Temporal Modelling |
Abstract | We present an extension of the linear time, time-bounded, Signal Temporal Logic to describe spatio-temporal properties. We consider a discrete location/ patch-based representation of space, with a population of interacting agents evolving in each location and with agents migrating from one patch to another one. We provide both a boolean and a quantitative semantics to this logic. We then present monitoring algorithms to check the validity of a formula, or to compute its satisfaction (robustness) score, over a spatio-temporal trace, exploiting these routines to do statistical model checking of stochastic models. We illustrate the logic at work on an epidemic example, looking at the diffusion of a cholera infection among communities living along a river. |
URL | http://eudl.eu/doi/10.4108/icst.valuetools.2014.258183 |
DOI | 10.4108/icst.valuetools.2014.258183 |