A Logical Framework for Reasoning About Local and Global Properties of Collective Systems

Collective adaptive systems (CAS) are composed of a large number of entities that interact with each other to reach local or global goals. Entities operate without any centralized control and should adapt their behavior to the changes in the environment where they operate. Due to the intricacies of these interactions and adaptation, it is difficult to predict the behavior of CAS. For this reason, formal tools are needed to specify and verify this behavior to ensure consistency, reliability, correctness, and safety properties. In this paper, we present a novel logical framework that permits specifying properties of CAS at both local and global levels: local properties refer to the behavior of individuals, while global properties refer to the whole system. An exact model checking algorithm, whose complexity is linear with the size of the formula and with the size of the model is also presented together with another one based on statistical model checking that permits handling systems composed by a large number of agents. Finally, a simple scenario is used to evaluate the advantages of the proposed approach.