Research Article
Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
@INPROCEEDINGS{10.4108/icst.valuetools.2014.258183, author={Laura Nenzi and Luca Bortolussi}, title={Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic}, proceedings={8th International Conference on Performance Evaluation Methodologies and Tools}, publisher={EAI}, proceedings_a={VALUETOOLS}, year={2015}, month={2}, keywords={monitoring spatial logic signal temporal logic spatio-temporal modelling}, doi={10.4108/icst.valuetools.2014.258183} }- Laura Nenzi
Luca Bortolussi
Year: 2015
Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
VALUETOOLS
ICST
DOI: 10.4108/icst.valuetools.2014.258183
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.
