An experimental spatio-temporal model checker

In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical verification framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the surrounded 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. The model checking algorithm that we propose features no particular efficiency optimisations, as it is meant to be a reference specification of a family of more efficient algorithms that are planned for future work. Its complexity depends on the product of temporal states and points of the space. Nevertheless, a prototype model checker has been implemented, made available, and used for experimentation of the application of spatio-temporal verification in the field of collective adaptive systems.