Analysis of Spatio-temporal Properties of Stochastic Systems Using TSTL
Copyright policy )Analysis of Spatio-temporal Properties of Stochastic Systems Using TSTL
In this article, 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 behavior 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 three-valued 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.
- University of Trieste Italy
- University of Camerino Italy
- University of Edinburgh United Kingdom
statistical model checking, stochastic spatial populationmodels, Specification and verification (program logics, model checking, etc.), Multi-valued logic, Stochastic spatial population models, Temporal logic, Statistical Model Checking, Probability and inductive logic, multi-valued logics, Multi-valued logics; Spatio-temporal logics; Statistical Model Checking; Stochastic spatial population models, spatio-temporal logics, stochastic spatial population models, Spatio-temporal logic, Verification by model checking, Spatio-temporal logics, Directional data; spatial statistics, Theory of computation
statistical model checking, stochastic spatial populationmodels, Specification and verification (program logics, model checking, etc.), Multi-valued logic, Stochastic spatial population models, Temporal logic, Statistical Model Checking, Probability and inductive logic, multi-valued logics, Multi-valued logics; Spatio-temporal logics; Statistical Model Checking; Stochastic spatial population models, spatio-temporal logics, stochastic spatial population models, Spatio-temporal logic, Verification by model checking, Spatio-temporal logics, Directional data; spatial statistics, Theory of computation
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).5 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!