{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,29]],"date-time":"2026-08-29T11:18:25Z","timestamp":1788002305900,"version":"build-2784847793"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T00:00:00Z","timestamp":1780444800000},"content-version":"vor","delay-in-days":2,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007514","name":"Universit\u00e0 di Pisa","doi-asserted-by":"publisher","award":["PRA_2022_99"],"award-info":[{"award-number":["PRA_2022_99"]}],"id":[{"id":"10.13039\/501100007514","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100021856","name":"Ministero dell\u2019Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["PRIN 20228KXFN2"],"award-info":[{"award-number":["PRIN 20228KXFN2"]}],"id":[{"id":"10.13039\/501100021856","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CNR (Italy); SRNSFG","award":["CNR-22-010"],"award-info":[{"award-number":["CNR-22-010"]}]},{"name":"CNR (Italy); SRNSFG","award":["PNRR PRI ECS00000017 PRR.AP008.003"],"award-info":[{"award-number":["PNRR PRI ECS00000017 PRR.AP008.003"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J of Log Lang and Inf"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows one to state properties about geometrical entities whose attributes change over time. For the given extension, we prove the equivalence of its operational semantics with a denotational one. We then introduce a temporal extension of the tool , a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams.<\/jats:p>","DOI":"10.1007\/s10849-026-09476-w","type":"journal-article","created":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T08:45:22Z","timestamp":1780476322000},"page":"83-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Spatio-temporal Model Checking with VoxLogicA"],"prefix":"10.1007","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1292-4086","authenticated-orcid":false,"given":"Laura","family":"Bussi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vincenzo","family":"Ciancia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabio","family":"Gadducci","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,3]]},"reference":[{"key":"9476_CR1","doi-asserted-by":"publisher","unstructured":"Aiello, M., Pratt-Hartmann, I., & Benthem, van, J. (2007). Handbook of Spatial Logics. Springer, Dordrecht. https:\/\/doi.org\/10.1007\/978-1-4020-5587-4","DOI":"10.1007\/978-1-4020-5587-4"},{"issue":"2","key":"9476_CR2","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-019-00511-9","volume":"22","author":"F Banci Buonamici","year":"2020","unstructured":"Banci Buonamici, F., Belmonte, G., Ciancia, V., Latella, D., & Massink, M. (2020). Spatial logics and model checking for medical imaging. Software Tools for Technology Transfer, 22(2), 195\u2013217.","journal-title":"Software Tools for Technology Transfer"},{"issue":"1","key":"9476_CR3","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1109\/TCNS.2016.2609138","volume":"5","author":"E Bartocci","year":"2016","unstructured":"Bartocci, E., Gol, E., Haghighi, I., & Belta, C. (2016). A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Transactions on Control of Network Systems, 5(1), 308\u2013320.","journal-title":"IEEE Transactions on Control of Network Systems"},{"key":"9476_CR4","doi-asserted-by":"publisher","unstructured":"Belmonte, G., Bussi, L., Ciancia, V., Latella, D., & Massink, M. (2024). Towards hybrid-AI in imaging using VoxLogicA. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024. LNCS, vol. 15222, pp. 205\u2013221. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-75387-9_13","DOI":"10.1007\/978-3-031-75387-9_13"},{"key":"9476_CR5","first-page":"1","volume-title":"FormaliSE@ICSE 2021","author":"G Belmonte","year":"2021","unstructured":"Belmonte, G., Broccia, G., Ciancia, V., Latella, D., & Massink, M. (2021). Feasibility of spatial model checking for nevus segmentation. In S. Bliudze, S. Gnesi, N. Plat, & L. Semini (Eds.), FormaliSE@ICSE 2021 (pp. 1\u201312). New York: IEEE."},{"key":"9476_CR6","series-title":"LNCS","first-page":"281","volume-title":"TACAS 2019","author":"G Belmonte","year":"2019","unstructured":"Belmonte, G., Ciancia, V., Latella, D., & Massink, M. (2019). VoxLogicA: A spatial model checker for declarative image analysis. LNCSIn T. Vojnar & L. Zhang (Eds.), TACAS 2019 (Vol. 11427, pp. 281\u2013298). Cham: Springer."},{"key":"9476_CR7","doi-asserted-by":"publisher","unstructured":"Belmonte, G., Ciancia, V., & Massink, M. (2025). Symbolic and hybrid AI for brain tissue segmentation using spatial model checking. Artif. Intell. Medicine, 167, 103154. https:\/\/doi.org\/10.1016\/J.ARTMED.2025.103154","DOI":"10.1016\/J.ARTMED.2025.103154"},{"issue":"3","key":"9476_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1020083231504","volume":"17","author":"B Bennett","year":"2002","unstructured":"Bennett, B., Cohn, A., Wolter, F., & Zakharyaschev, M. (2002). Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Applied Intelligence, 17(3), 239\u2013251. https:\/\/doi.org\/10.1023\/A:1020083231504","journal-title":"Applied Intelligence"},{"key":"9476_CR9","first-page":"187","volume-title":"Advances in Modal Logic","author":"N Bezhanishvili","year":"2024","unstructured":"Bezhanishvili, N., Bussi, L., Ciancia, V., Fern\u00e1ndez-Duque, D., & Gabelaia, D. (2024). Logics of polyhedral reachability. In A. Ciabattoni, D. Gabelaia, & I. Sedl\u00e1r (Eds.), Advances in Modal Logic (Vol. 15, pp. 187\u2013204). London: College Publications."},{"issue":"4","key":"9476_CR10","first-page":"7","volume":"18","author":"N Bezhanishvili","year":"2022","unstructured":"Bezhanishvili, N., Ciancia, V., Gabelaia, D., Grilletti, G., Latella, D., & Massink, M. (2022). Geometric model checking of continuous space. Logical Methods in Computer Science, 18(4), 7\u20131738.","journal-title":"Logical Methods in Computer Science"},{"key":"9476_CR11","doi-asserted-by":"publisher","unstructured":"Bussi, L., Ciancia, V., & Gadducci, F. (2023). A spatial logic with time and quantifiers. In: Gierasimczuk, N., Vel\u00e1zquez-Quesada, F.R. (eds.) DaL\u00ed 2023. LNCS, vol. 14401, pp. 1\u201319. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-51777-8_1","DOI":"10.1007\/978-3-031-51777-8_1"},{"key":"9476_CR12","series-title":"LNCS","first-page":"188","volume-title":"FORTE 2021","author":"L Bussi","year":"2021","unstructured":"Bussi, L., Ciancia, V., & Gadducci, F. (2021). Towards a spatial model checker on GPU. LNCSIn K. Peters & T. A. C. Willemse (Eds.), FORTE 2021 (Vol. 12719, pp. 188\u2013196). Cham: Springer."},{"key":"9476_CR13","series-title":"LNCS","first-page":"78","volume-title":"DataMod 2021","author":"L Bussi","year":"2022","unstructured":"Bussi, L., Ciancia, V., Gadducci, F., Latella, D., & Massink, M. (2022). Towards model checking video streams using VoxLogicA on GPUs. LNCSIn J. Bowles, G. Broccia, & R. Pellungrini (Eds.), DataMod 2021 (Vol. 13268, pp. 78\u201390). Cham: Springer."},{"key":"9476_CR14","series-title":"LNCS","first-page":"479","volume-title":"ISoLA 2022","author":"L Bussi","year":"2022","unstructured":"Bussi, L., Ciancia, V., Gadducci, F., Latella, D., & Massink, M. (2022). On binding in the spatial logics for closure spaces. LNCSIn T. Margaria & B. Steffen (Eds.), ISoLA 2022 (Vol. 13701, pp. 479\u2013497). Cham: Springer."},{"key":"9476_CR15","volume-title":"Topological Spaces","author":"E \u010cech","year":"1966","unstructured":"\u010cech, E., Frol\u00edk, Z., & Kat\u011btov, M. (1966). Topological Spaces. Publishing House of the Czechoslovak Academy of Sciences, Prague: Academia."},{"key":"9476_CR16","doi-asserted-by":"publisher","unstructured":"Ciancia, V., Latella, D., Loreti, M., & Massink, M. (2014). Specifying and verifying properties of space. In: D\u00edaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222\u2013235. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-662-44602-7_18","DOI":"10.1007\/978-3-662-44602-7_18"},{"issue":"3","key":"9476_CR17","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10009-018-0483-8","volume":"20","author":"V Ciancia","year":"2018","unstructured":"Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., & Massink, M. (2018). Spatio-temporal model checking of vehicular movement in public transport systems. Software Tools for Technology Transfer, 20(3), 289\u2013311.","journal-title":"Software Tools for Technology Transfer"},{"key":"9476_CR18","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Latella, D., Loreti, M., & Massink, M. (2016). Model checking spatial logics for closure spaces. Logical Methods in Computer Science, 12(4),","DOI":"10.2168\/LMCS-12(4:2)2016"},{"key":"9476_CR19","series-title":"LNCS","first-page":"657","volume-title":"ISoLA 2016","author":"V Ciancia","year":"2016","unstructured":"Ciancia, V., Latella, D., Massink, M., Pa\u0161kauskas, R., & Vandin, A. (2016). A tool-chain for statistical spatio-temporal model checking of bike sharing systems. LNCSIn T. Margaria & B. Steffen (Eds.), ISoLA 2016 (Vol. 9952, pp. 657\u2013673). Cham: Springer."},{"key":"9476_CR20","doi-asserted-by":"publisher","unstructured":"Gabelaia, D., Kontchakov, R., Kurucz, A., Wolter, F., & Zakharyaschev, M. (2005). Combining spatial and temporal logics: Expressiveness vs. complexity. Artificial Intelligence Research, 23, 167\u2013243. https:\/\/doi.org\/10.1613\/jair.1537","DOI":"10.1613\/jair.1537"},{"issue":"1\u20133","key":"9476_CR21","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0304-3975(02)00701-6","volume":"305","author":"A Galton","year":"2003","unstructured":"Galton, A. (2003). A generalized topological view of motion in discrete space. Theoretical Computer Science, 305(1\u20133), 111\u2013134.","journal-title":"Theoretical Computer Science"},{"key":"9476_CR22","volume-title":"The Stanford Encyclopedia of Philosophy, Spring","author":"J Garson","year":"2024","unstructured":"Garson, J. (2024). Modal Logic. In E. N. Zalta & U. Nodelman (Eds.), The Stanford Encyclopedia of Philosophy, Spring (2024th ed.). Metaphysics Research Lab: Stanford University, Stanford.","edition":"2024"},{"key":"9476_CR23","first-page":"854","volume-title":"IJCAI 2013","author":"GD Giacomo","year":"2013","unstructured":"Giacomo, G. D., & Vardi, M. Y. (2013). Linear temporal logic and linear dynamic logic on finite traces. In F. Rossi (Ed.), IJCAI 2013 (pp. 854\u2013860). New York: IJCAI\/AAAI."},{"issue":"1","key":"9476_CR24","doi-asserted-by":"publisher","first-page":"141","DOI":"10.2307\/1969080","volume":"45","author":"JCC McKinsey","year":"1944","unstructured":"McKinsey, J. C. C., & Tarski, A. (1944). The algebra of topology. Annals of Mathematics, 45(1), 141\u2013191.","journal-title":"Annals of Mathematics"},{"key":"9476_CR25","doi-asserted-by":"publisher","unstructured":"Nenzi, L., Bartocci, E., Bortolussi, L., & Loreti, M. (2022). A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. Logical Methods in Computer Science 18(1) https:\/\/doi.org\/10.46298\/lmcs-18(1:4)2022","DOI":"10.46298\/lmcs-18(1:4)2022"},{"key":"9476_CR26","doi-asserted-by":"crossref","unstructured":"Tsigkanos, C., Kehrer, T., & Ghezzi, C. (2017). Modeling and verification of evolving cyber-physical spaces. In E. Bodden, W. Sch\u00e4fer, A. Deursen, & A. Zisman (Eds.), ESEC\/FSE 2017 (pp. 38\u201348). New York, NY, USA: ACM.","DOI":"10.1145\/3106237.3106299"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-026-09476-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10849-026-09476-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-026-09476-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,29]],"date-time":"2026-08-29T11:02:54Z","timestamp":1788001374000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10849-026-09476-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":26,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["9476"],"URL":"https:\/\/doi.org\/10.1007\/s10849-026-09476-w","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"value":"0925-8531","type":"print"},{"value":"1572-9583","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"14 February 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 June 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare no conflict of interest.","order":1,"name":"Ethics","label":"Conflict of interest","group":{"name":"EthicsHeading","label":"Declarations"}}]}}