A spatio-temporal model-checker

We define a spatio-temporal logic, the Spatio-temporal Logic of Closure Spaces (STLCS). The logic is interpreted on Kripke models, in which each state has an associated closure space. The logic extends CTL with spatial operators, in the spirit of topological modal logic. More specifically, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the spatial until operator, with its intended meaning of a point being surrounded by entities satisfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. We present a simple model-checking algorithm for STLCS, which has been implemented in a prototype tool.