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|
|Series||EAI ENDORSED TRANSACTIONS ON CLOUD SYSTEMS|
|Keywords||Monitoring, Signal Temporal Logic, Spatial Logic, Spatio-Temporal Modelling|
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.