Collective adaptive systems (CAS) are composed of many entities that interact with each other to reach local or global goals. In CAS, two kinds of behaviour can be considered: local behaviour and global behaviour. The former is the behaviour of each entity operating in the system. The latter is the system’s behaviour as a whole and emerges from the local computations. Many languages have been proposed to model CAS to forecast the effect of local computations at the global level. Moreover, logics and tools have also been proposed to specify the properties of collectives and verify their satisfaction. Unfortunately, due to the problem of state-space explosion, standard exact model-checking techniques cannot be used. This paper presents a methodology that supports scalable analysis of CAS. Based on mean-field approximation, the proposed technique can be used to verify the behaviour of the single agents in a context approximated in terms of a deterministic process. A simple example shows how the proposed approach can be used to support the analysis of CAS.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Scalable Verification of Local and Global Properties of Collective Systems

  • Michele Loreti,
  • Michela Quadrini,
  • Aniqa Rehman

摘要

Collective adaptive systems (CAS) are composed of many entities that interact with each other to reach local or global goals. In CAS, two kinds of behaviour can be considered: local behaviour and global behaviour. The former is the behaviour of each entity operating in the system. The latter is the system’s behaviour as a whole and emerges from the local computations. Many languages have been proposed to model CAS to forecast the effect of local computations at the global level. Moreover, logics and tools have also been proposed to specify the properties of collectives and verify their satisfaction. Unfortunately, due to the problem of state-space explosion, standard exact model-checking techniques cannot be used. This paper presents a methodology that supports scalable analysis of CAS. Based on mean-field approximation, the proposed technique can be used to verify the behaviour of the single agents in a context approximated in terms of a deterministic process. A simple example shows how the proposed approach can be used to support the analysis of CAS.