A Spatial Logic with Time and Quantifiers

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 extend SLCS in two directions. We first introduce first-order quantifiers, ranging 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 geometrical entities whose attributes change along time. For both extensions, we prove the equivalence of their operational semantics with a denotational one.