{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:28:41Z","timestamp":1750220921617,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T00:00:00Z","timestamp":1572480000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Austrian Science Fund (FWF) for the project ZK 35"},{"name":"Microsoft Research Cambridge through its PhD Scholarship Programme"},{"name":"EU project QUANTICOL","award":["600708"],"award-info":[{"award-number":["600708"]}]},{"name":"Scottish Government Rural and Environment Science and Analytical Services Division"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3326168","type":"journal-article","created":{"date-parts":[[2019,12,11]],"date-time":"2019-12-11T13:27:18Z","timestamp":1576070838000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Analysis of Spatio-temporal Properties of Stochastic Systems Using TSTL"],"prefix":"10.1145","volume":"29","author":[{"given":"Ludovica Luisa","family":"Vissat","sequence":"first","affiliation":[{"name":"School of Informatics, University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3061-863X","authenticated-orcid":false,"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[{"name":"School of Science and Technology, University of Camerino, Camerino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Nenzi","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Geosciences, University of Trieste, Trieste, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4914-9255","authenticated-orcid":false,"given":"Jane","family":"Hillston","sequence":"additional","affiliation":[{"name":"School of Informatics, University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Glenn","family":"Marion","sequence":"additional","affiliation":[{"name":"Biomathematics and Statistics Scotland, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,10]]},"reference":[{"volume-title":"Handbook of Spatial Logics","author":"Aiello Marco","key":"e_1_2_1_1_1","unstructured":"Marco Aiello , Ian Pratt-Hartmann , and Johan Van Benthem . 2007. Handbook of Spatial Logics . Springer Netherlands . Marco Aiello, Ian Pratt-Hartmann, and Johan Van Benthem. 2007. Handbook of Spatial Logics. Springer Netherlands."},{"key":"e_1_2_1_2_1","volume-title":"A rewriting-based model checker for the linear temporal logic of rewriting. Electronic Notes in Theoretical Computer Science 290 (Dec","author":"Bae Kyungmin","year":"2012","unstructured":"Kyungmin Bae and Jos\u00e9 Meseguer . 2012. A rewriting-based model checker for the linear temporal logic of rewriting. Electronic Notes in Theoretical Computer Science 290 (Dec . 2012 ), 19--36. DOI:https:\/\/doi.org\/10.1016\/j.entcs.2012.11.009 10.1016\/j.entcs.2012.11.009 Kyungmin Bae and Jos\u00e9 Meseguer. 2012. A rewriting-based model checker for the linear temporal logic of rewriting. Electronic Notes in Theoretical Computer Science 290 (Dec. 2012), 19--36. DOI:https:\/\/doi.org\/10.1016\/j.entcs.2012.11.009"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264250"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127050"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020083231504"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2010.22"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45465-9_51"},{"volume-title":"Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201900)","author":"Cardelli Luca","key":"e_1_2_1_10_1","unstructured":"Luca Cardelli and Andrew D. Gordon . 2000. Anytime, anywhere: Modal logics for mobile ambients . In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201900) . ACM, New York, 365--377. DOI:https:\/\/doi.org\/10.1145\/325694.325742 10.1145\/325694.325742 Luca Cardelli and Andrew D. Gordon. 2000. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201900). ACM, New York, 365--377. DOI:https:\/\/doi.org\/10.1145\/325694.325742"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1600-0587.2011.07190.x"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15784-4_9"},{"volume-title":"Specifying and verifying properties of space","author":"Ciancia Vincenzo","key":"e_1_2_1_13_1","unstructured":"Vincenzo Ciancia , Diego Latella , Michele Loreti , and Mieke Massink . 2014. Specifying and verifying properties of space . In Theoretical Computer Science, Josep Diaz, Ivan Lanese, and Davide Sangiorgi (Eds.). Springer , Berlin , 222--235. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2014. Specifying and verifying properties of space. In Theoretical Computer Science, Josep Diaz, Ivan Lanese, and Davide Sangiorgi (Eds.). Springer, Berlin, 222--235."},{"volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems (Lecture Notes in Computer Science)","author":"Ciancia Vincenzo","key":"e_1_2_1_14_1","unstructured":"Vincenzo Ciancia , Diego Latella , Michele Loreti , and Mieke Massink . 2016. Spatial logic and spatial model checking for closure spaces . In Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems (Lecture Notes in Computer Science) . Springer , Cham , 156--201. DOI:https:\/\/doi.org\/10.1007\/978-3-319-34096-8_6 10.1007\/978-3-319-34096-8_6 Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2016. Spatial logic and spatial model checking for closure spaces. In Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems (Lecture Notes in Computer Science). Springer, Cham, 156--201. DOI:https:\/\/doi.org\/10.1007\/978-3-319-34096-8_6"},{"key":"e_1_2_1_15_1","first-page":"1","article-title":"Static BiLog: A unifying language for spatial structures","volume":"80","author":"Conforti Giovanni","year":"2007","unstructured":"Giovanni Conforti , Damiano Macedonio , and Vladimiro Sassone . 2007 . Static BiLog: A unifying language for spatial structures . Fundamenta Informaticae 80 , 1 -- 3 (2007), 91--110. http:\/\/dblp.uni-trier.de\/db\/journals\/fuin\/fuin80.html#ConfortiMS07 Giovanni Conforti, Damiano Macedonio, and Vladimiro Sassone. 2007. Static BiLog: A unifying language for spatial structures. Fundamenta Informaticae 80, 1--3 (2007), 91--110. http:\/\/dblp.uni-trier.de\/db\/journals\/fuin\/fuin80.html#ConfortiMS07","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.05.008"},{"volume-title":"Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science (Lecture Notes in Computer Science), Christian Freksa and David M","author":"Galton Antony","key":"e_1_2_1_17_1","unstructured":"Antony Galton . 1999. The mereotopology of discrete space . In Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science (Lecture Notes in Computer Science), Christian Freksa and David M . Mark (Eds.). Springer , Berlin . Antony Galton. 1999. The mereotopology of discrete space. In Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science (Lecture Notes in Computer Science), Christian Freksa and David M. Mark (Eds.). Springer, Berlin."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1021\/j100540a008"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039367"},{"volume-title":"Stanford Encyclopedia of Philosophy.","author":"Gottwald Siegfried","key":"e_1_2_1_20_1","unstructured":"Siegfried Gottwald . 2008. Many-valued logic . In Stanford Encyclopedia of Philosophy. Siegfried Gottwald. 2008. Many-valued logic. In Stanford Encyclopedia of Philosophy."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728633"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.3733\/hilg.v27n14p343"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.09.007"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.03.007"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/2267778"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspb.2016.1170"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3150928.3150961"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings 14th International Workshopon Quantitative Aspects of Programming Languages and Systems (Electronic Proceedings in Theoretical Computer Science)","volume":"227","author":"Vissat Ludovica Luisa","unstructured":"Ludovica Luisa Vissat , Jane Hillston , Glenn Marion , and Matthew J. Smith . 2016. MELA: Modelling in ecology with location attributes . In Proceedings 14th International Workshopon Quantitative Aspects of Programming Languages and Systems (Electronic Proceedings in Theoretical Computer Science) , Vol. 227 . 82--97. DOI:https:\/\/doi.org\/10.4204\/EPTCS.227.6 10.4204\/EPTCS.227.6 Ludovica Luisa Vissat, Jane Hillston, Glenn Marion, and Matthew J. Smith. 2016. MELA: Modelling in ecology with location attributes. In Proceedings 14th International Workshopon Quantitative Aspects of Programming Languages and Systems (Electronic Proceedings in Theoretical Computer Science), Vol. 227. 82--97. DOI:https:\/\/doi.org\/10.4204\/EPTCS.227.6"},{"volume-title":"Quantitative Evaluation of Systems (QEST\u201917)","author":"Vissat Ludovica Luisa","key":"e_1_2_1_31_1","unstructured":"Ludovica Luisa Vissat , Michele Loreti , Laura Nenzi , Jane Hillston , and Glenn Marion . 2017. Three-valued spatio-temporal logic: A further analysis on spatio-temporal properties of stochastic systems . In Quantitative Evaluation of Systems (QEST\u201917) , Nathalie Bertrand and Luca Bortolussi (Eds.). Springer International Publishing , 317--332. DOI:https:\/\/doi.org\/10.1007\/978-3-319-66335-7_22 10.1007\/978-3-319-66335-7_22 Ludovica Luisa Vissat, Michele Loreti, Laura Nenzi, Jane Hillston, and Glenn Marion. 2017. Three-valued spatio-temporal logic: A further analysis on spatio-temporal properties of stochastic systems. In Quantitative Evaluation of Systems (QEST\u201917), Nathalie Bertrand and Luca Bortolussi (Eds.). Springer International Publishing, 317--332. DOI:https:\/\/doi.org\/10.1007\/978-3-319-66335-7_22"},{"volume-title":"Selected Works","author":"\u0141ukasiewicz Jan","key":"e_1_2_1_32_1","unstructured":"Jan \u0141ukasiewicz . 1970. Selected Works . Amsterdam : North-Holland Pub. Co . Jan \u0141ukasiewicz. 1970. Selected Works. Amsterdam: North-Holland Pub. Co."},{"key":"e_1_2_1_33_1","volume-title":"Modelling and Analysis of Timed and Fault-Tolerant Systems: Joint International Conferences on Formal Modeling and Analysis of Timed Systmes (FORMATS\u201904)","author":"Maler Oded","year":"2004","unstructured":"Oded Maler and Dejan Nickovic . 2004 . Monitoring temporal properties of continuous signals. In Formal Techniques , Modelling and Analysis of Timed and Fault-Tolerant Systems: Joint International Conferences on Formal Modeling and Analysis of Timed Systmes (FORMATS\u201904) , and Formal Techniques in Real-Time and Fault -Tolerant Systems (FTRTFT\u201904). Proceedings. Springer, Berlin, 152--166. DOI:https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12 10.1007\/978-3-540-30206-3_12 Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems: Joint International Conferences on Formal Modeling and Analysis of Timed Systmes (FORMATS\u201904), and Formal Techniques in Real-Time and Fault -Tolerant Systems (FTRTFT\u201904). Proceedings. Springer, Berlin, 152--166. DOI:https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.66.051915"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.6.897"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_22"},{"volume-title":"Runtime Verification - 6th International Conference (RV\u201915). 21--37. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23820-3_2","author":"Nenzi Laura","key":"e_1_2_1_37_1","unstructured":"Laura Nenzi , Luca Bortolussi , Vincenzo Ciancia , Michele Loreti , and Mieke Massink . 2015. Qualitative and quantitative monitoring of spatio-temporal properties . In Runtime Verification - 6th International Conference (RV\u201915). 21--37. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23820-3_2 10.1007\/978-3-319-23820-3_2 Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. 2015. Qualitative and quantitative monitoring of spatio-temporal properties. In Runtime Verification - 6th International Conference (RV\u201915). 21--37. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23820-3_2"},{"key":"e_1_2_1_38_1","volume-title":"10th EAI International Conference on Performance Evaluation Methodologies and Tools.","author":"Nenzi Laura","year":"2016","unstructured":"Laura Nenzi , Luca Bortolussi , and Michele Loreti . 2016 . jSSTL - A tool to monitor spatio-temporal properties . In 10th EAI International Conference on Performance Evaluation Methodologies and Tools. Laura Nenzi, Luca Bortolussi, and Michele Loreti. 2016. jSSTL - A tool to monitor spatio-temporal properties. In 10th EAI International Conference on Performance Evaluation Methodologies and Tools."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90003-0"},{"key":"#cr-split#-e_1_2_1_40_1.1","doi-asserted-by":"crossref","unstructured":"Koushik Sen Mahesh Viswanathan and Gul Agha. 2006. Model-checking Markov chains in the presence of uncertainties. In Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference (TACAS'06) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS'06). Proceedings. Springer Berlin 394--410. DOI:https:\/\/doi.org\/10.1007\/11691372_26 10.1007\/11691372_26","DOI":"10.1007\/11691372_26"},{"key":"#cr-split#-e_1_2_1_40_1.2","doi-asserted-by":"crossref","unstructured":"Koushik Sen Mahesh Viswanathan and Gul Agha. 2006. Model-checking Markov chains in the presence of uncertainties. In Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference (TACAS'06) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS'06). Proceedings. Springer Berlin 394--410. DOI:https:\/\/doi.org\/10.1007\/11691372_26","DOI":"10.1007\/11691372_26"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326168","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3326168","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:08Z","timestamp":1750204388000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326168"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,31]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3326168"],"URL":"https:\/\/doi.org\/10.1145\/3326168","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"type":"print","value":"1049-3301"},{"type":"electronic","value":"1558-1195"}],"subject":[],"published":{"date-parts":[[2019,10,31]]},"assertion":[{"value":"2018-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-12-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}