Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic

TitleSpecifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
Publication TypeConference Paper
Year of Publication2015
AuthorsBortolussi L, Nenzi L
Conference NameVALUETOOLS2014
Volume1
SeriesEAI ENDORSED TRANSACTIONS ON CLOUD SYSTEMS
Issue4
KeywordsMonitoring, 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. 

URLhttp://eudl.eu/doi/10.4108/icst.valuetools.2014.258183
DOI10.4108/icst.valuetools.2014.258183