Edinburgh Research Explorer

Analysis of spatio-temporal properties of stochastic systems using TSTL

Research output: Contribution to journalArticle

  • Ludovica Luisa Vissat
  • Michele Loreti
  • Laura Nenzi
  • Jane Hillston
  • Glenn Marion

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://dl.acm.org/citation.cfm?id=3326168
Original languageEnglish
Article number20
Pages (from-to)20:1-20:24
Number of pages25
JournalACM Transactions on Modeling and Computer Simulation
Volume29
Issue number4
DOIs
Publication statusPublished - 13 Dec 2019

Abstract

In this paper, we present Three-Valued Spatio-Temporal Logic (TSTL), which enriches the available spatiotemporal analysis of properties expressed in Signal Spatio-Temporal Logic (SSTL), to give further insight into the dynamic behaviour of systems. Our novel analysis starts from the estimation of satisfaction probabilities of given SSTL properties and allows the analysis of their temporal and spatial evolution. Moreover, in our verification procedure, we use a three-valued approach to include the intrinsic and unavoidable uncertainty related to the simulation-based statistical evaluation of the estimates; this can be also used to assess the appropriate number of simulations to use depending on the analysis needs. We present the syntax and threevalued semantics of TSTL and specific extended monitoring algorithms to check the validity of TSTL
formulas. We introduce a reliability requirement for TSTL monitoring and an automatic procedure to verify it. Two case studies demonstrate how TSTL broadens the application of spatio-temporal logics in realistic scenarios, enabling analysis of threat monitoring and privacy preservation based on spatial stochastic population models.

    Research areas

  • Theory of computation, Verification by model checking, Spatio-temporal logics, multi-valued logics, stochastic spatial populationmodels, Statistical Model Checking

Download statistics

No data available

ID: 92041249