Spatio-temporal model-checking for collective adaptive systems in QUANTICOL

Spatial aspects of computation are becoming increasingly relevant when dealing with systems distributed in physical space. Traditionalformal 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 firnded 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.