Automatic verification of reliability requirements of spatio-temporal analysis using Three-Valued Spatio-Temporal Logic

In this paper we present the recently introduced Three-Valued Spatio-Temporal Logic (TSTL), which extends the available spatio-temporal analysis of stochastic systems, and an automatic procedure to verify whether this analysis satisfies given reliability requirements. The novel spatio-temporal logic TSTL enriches the analysis of properties expressed in Signal Spatio-Temporal Logic (SSTL), providing further insight into the dynamic behaviour of systems. Starting from the estimated satisfaction probabilities of given SSTL properties, it enables the analysis of their temporal and spatial evolution. We use a three-valued approach in our verification procedure to include the uncertainty associated with the simulation-based statistical method used to estimate the satisfaction probabilities. In relation to this aspect, we introduce a reliability specification for the TSTL analysis and we present a specific algorithm to automatically assess whether it is satisfied by the evaluation of TSTL formulas.