A spatial logic with time and quantifiers

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.