Specifying and verifying properties of space

Ciancia V., Latella D., Loreti M., Massink M.

Model logics  Spatial logics  Topological spaces  Specifying and verifying and reasoning about programs soggetto  Mathematical logic  Software/Program verification 

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.

Source: ISTI Technical reports, 2014