Title: Automated analysis of compositional multi-agent systems
Author: Alexei Sharpanskykh, Jan Treur
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.
Int. J. of Agent-Oriented Software Engineering, 2010 Vol.4, No.2, pp.174 - 221
Date of acceptance: 19 Nov 2009
Available online: 22 Apr 2010