Specifying and verifying properties of space

The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the eld of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verica- tion techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not explicitly taken into account. We propose a methodology to verify prop- erties depending upon physical space. We dene an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological denitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We further extend the frame- work with a spatial until operator, and dene an ecient model checking procedure, implemented in a proof-of-concept tool.