EAI Endorsed Transactions on Cloud Systems 15(4): e4

Research Article

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

Download44 downloads
  • @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={15},
        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
Laura Nenzi1,*, Luca Bortolussi2
  • 1: IMT, Lucca, Italy
  • 2: DMG, University of Trieste, Italy
*Contact email: laura.nenzi@imtlucca.it

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.