Spatio-temporal model checking with VoxLogicA

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 VoxLogicA, a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams.