Monitoring Local and Global Properties of Collective Adaptive Systems

Collective adaptive systems (CAS) are composed of many entities that interact with each other to reach local or global goals. Entities operate without any centralized control and should adapt their behaviour according to the changes in the environment where they operate. For CAS, it is crucial to introduce tools and methodologies that permit specifying and verifying properties of the expected behaviour. The logic GLoTL has been introduced to specify properties of CAS at both local and global levels. At a local level, the properties of the behaviour of single entities are considered. While at the global level, properties refer to the whole system. This paper introduces an algorithm supporting runtime verification of GLoTL. Moreover, thanks to its integration in the tool Sibilla, we will show how the proposed methodology can used to verify the behaviour of classical CAS examples specified via the language YODA.