Research Article
Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
@ARTICLE{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}, journal={EAI Endorsed Transactions on Cloud Systems}, volume={1}, number={4}, publisher={EAI}, journal_a={CS}, 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
CS
EAI
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.
Copyright © 2015 L. Nenzi and L. Bortolussi, licensed to EAI. This is an open access article distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/3.0/), which permits unlimited use, distribution and reproduction in any medium so long as the original work is properly cited.
