Automated analysis of compositional multi-agent systems

An approach for handling the complex dynamics of a multi-agent system is based on distinguishing aggregation levels. The behaviour at a given aggregation level is specified by a set of dynamic properties at that level, expressed in some (temporal) language. Such behavioural specifications may be complex and difficult to analyse. To enable automated analysis of system specifications, a simpler format is required. To this end, a specification at a lower aggregation level can be created, describing basic steps in the processes of a system. This paper presents a method and tool to support the automated creation of such a specification, as a refinement of a given higher level specification. The generated specification has a simple format which can easily be used for analysis. This paper describes an approach for automated verification of logical consequences of specifications using model checking techniques.

• Type: Journal
• Year: 2010
• Where: IJAOSE
• Authors: Alexei Sharpanskykh, Jan Treur
• Keywords: Aggregation Level, IJAOSE 2010, Lower Aggregation Level, Specifications