Bussi L., Ciancia V., Gadducci F.
Finite traces Spatial logics Model checking Video stream analysis Spatial Logics Quantified Temporal Logics
Spatial logics are formalisms for expressing topological prop erties 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 extend SLCS in two directions. We first introduce first-order quantifiers, rang ing on both individuals and atomic propositions. We then equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows to state properties about geomet rical entities whose attributes change along time. For both extensions, we prove the equivalence of their operational semantics with a denotational one.
Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14401, pp. 1-19
@inbook{oai:iris.cnr.it:20.500.14243/509053, title = {A spatial logic with time and quantifiers}, author = {Bussi L. and Ciancia V. and Gadducci F.}, doi = {10.1007/978-3-031-51777-8_1}, booktitle = {LECTURE NOTES IN COMPUTER SCIENCE, vol. 14401, pp. 1-19}, year = {2024} }