Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
Journal Title: EAI Endorsed Transactions on Cloud Systems - Year 2015, Vol 1, Issue 4
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.
Authors and Affiliations
Laura Nenzi, Luca Bortolussi
Keywords
Related Articles
- EP ID EP45567
- DOI http://dx.doi.org/10.4108/icst.valuetools.2014.258183
- Views 301
- Downloads 0
A scalable middleware-based infrastructure for energy management and visualization in city districts
Following the Smart City views, citizens, policy makers and energy distribution companies need a reliable and scalable infrastructure to manage and analyse energy consumption data in a city district context. In order to...
A New QoE-Driven Video Cache Allocation Scheme for Mobile Cloud Server
With the advent of mobile cloud computing, video cache technologies at local cellular networks have attracted extensive attention. Nevertheless, existing video cache allocation schemes mostly made decisions only accordin...
Specification of REST API Services for Modbus Protocol using Formal technique
With the advancements in technologies, there has been a growing trend to move from desktop applications towards web and mobile applications. This move was made possible through introduction of the RESTful Web Services. T...
Social Aspect of Vehicular Communications
The interconnection of devices is expected to grow and to incorporate systems that used to be isolated. As the vehicle evolves from a simple transport machine to an intelligent entity that collects information from the e...
Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic
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 interacti...