Spatio-temporal model-checking for collective adaptive systems

Spatial aspects of computation are becoming increasingly relevant when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of system models; however, properties of space are typically not taken into account explicitly. In this position paper we briefly review some of the recent developments of spatial and spatio-temporal model-checking in the context of the European research project QUANTICOL funded by the FET-Proactive programme on Fundamentals of Collective Adaptive Systems. We illustrate some typical applications of spatial and spatio-temporal model checking on collective adaptive systems and provide an outline for further developments.