Three-Valued Spatio-Temporal Logic: A Further Analysis on Spatio-Temporal Properties of Stochastic Systems
Autor: | Jane Hillston, Laura Nenzi, Ludovica Luisa Vissat, Michele Loreti, Glenn Marion |
---|---|
Přispěvatelé: | Nathalie Bertrand, Luca Bortolussi, LUISA VISSAT, Ludovica, Loreti, Michele, Nenzi, Laura, Hillston, Jane, Marion, Glenn |
Rok vydání: | 2017 |
Předmět: |
Syntax (programming languages)
Computer science Computer Science (all) SIGNAL (programming language) Theoretical Computer Science 0102 computer and information sciences 02 engineering and technology computer.software_genre Semantics 01 natural sciences Monitoring and control Verification procedure Population model 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Spatial evolution 020201 artificial intelligence & image processing Temporal logic Data mining computer |
Zdroj: | Quantitative Evaluation of Systems ISBN: 9783319663340 QEST Luisa Vissat, L, Loreti, M, Nenzi, L, Hillston, J & Marion, G 2017, Three-Valued Spatio-Temporal Logic: a further analysis on spatio-temporal properties of stochastic systems . in Quantitative Evaluation of Systems. QEST 2017. . Lecture Notes in Computer Scienc, vol. 10503, pp. 317-332, 14th International Conference on Quantitative Evaluation of Systems, Berlin, Germany, 5/09/17 . https://doi.org/10.1007/978-3-319-66335-7_22 |
DOI: | 10.1007/978-3-319-66335-7_22 |
Popis: | In this paper we present Three-Valued Spatio-Temporal Logic (TSTL), which enriches the available spatio-temporal 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 three-valued semantics of TSTL and aspecific extended monitoring algorithm to check the validity of TSTL formulas.We conclude with two case studies that demonstrate how TSTL broadens the application of spatio-temporal logics in realistic scenarios, enabling analysis of threat monitoring and control programmes based on spatial stochastic population models. |
Databáze: | OpenAIRE |
Externí odkaz: |