Title: Automated analysis of compositional multi-agent systems

Authors: Alexei Sharpanskykh, Jan Treur

Addresses: Artificial Intelligence Department, Vrije Universiteit Amsterdam, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands. ' Artificial Intelligence Department, Vrije Universiteit Amsterdam, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands

Abstract: 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.

Keywords: automated analysis; multi-agent systems; compositional modelling; MAS modelling; compositional verification; model checking; automated transformation; behavioural specifications; temporal modelling; temporal analysis; executable format; transition systems; agent-based systems.

DOI: 10.1504/IJAOSE.2010.032801

International Journal of Agent-Oriented Software Engineering, 2010 Vol.4 No.2, pp.174 - 221

Accepted: 19 Nov 2009
Published online: 22 Apr 2010 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article