Specification and Verification of Local and Global Properties of Collective Systems

Collective Adaptive Systems (CAS) are composed of a huge amount of components that interact with each other and with the enclosing environment to reach local and global goals. Each component in the system may exhibit autonomic behaviour depending on its properties, objectives, and actions. Decision-making in such systems is complicated, and interaction between components may introduce new and sometimes unexpected behaviours. Due to the intricacies of these interactions and adaptation, it is difficult to predict the behaviour of CAS. For this reason, formal tools are needed to specify and verify this behaviour to ensure consistency, reliability, correctness, and safety properties. Different models and formalisms have been proposed to describe CAS, but these systems are mainly considered from a global perspective where the behaviour of the single component somehow disappears in the multitude of the system state. This thesis aims to introduce a novel framework that specifies and verifies CAS properties at both global and local level. We present a Multi-Agent Discrete Time Model (MADTM) that is used to render the behaviour of a system composed of a multitude of agents by providing both global and local perspectives. We model the agent’s behaviour at different levels of abstraction that permit us to describe the comprehensive details of the system. We also present Global and Local Temporal Logic (GLoTL) a temporal logic that permits specifying both global and local properties of multi-agent systems described as MADTM models. Local properties capture the behaviour of individual agents and describe how the individual agent behaviour influences the system’s behavior at a global level, while global properties permit us to describe the system’s overall behaviour. We also introduced the model- checking algorithms to verify the proposed properties. For this purpose, we first introduce an exact model-checking algorithm to check if a given GLoTL formula is verified or not. Our approach is linear with the formula size Φ, but we presented a statistical model-checking approach due to state-space issues. Moreover, we propose a scalable analysis technique to approximate the interaction among individual components. This technique permits the analysis of systems with a large number of components, where explicit modelling of interactions becomes impractical. We extended our framework by imple- menting the mean-field analysis technique to reduce the system’s complexity. For this purpose, we extend our GLoTL logic to GLoTL+ with branching time constructs like PCTL to describe the system properties from a global perspective and about single agent behaviour operating in a global context. Our proposed framework highlights the local and global model-checking tech- nique with the deterministic mean-field approximation in discrete time. We implement this framework in a tool called Sibilla, a modular tool developed in Java to support the quantitative analysis of CAS. This tool is considered a container where new components can be easily added to integrate new analysis techniques and specification languages. This thesis focused on the Language of Interacting Objects (LIO) to generate the Discrete Time Model. Finally, we present some simple scenarios to evaluate the advantages of the proposed approach.