Automated Analysis of Compositional Multi-Agent Systems

O. Sharpanskykh, J. Treur

Research output: Contribution to JournalArticleAcademicpeer-review

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. Copyright © 2010 Inderscience Enterprises Ltd.
Original languageEnglish
Pages (from-to)174-221
JournalInternational Journal of Agent-Oriented Software Engineering
Volume4
Issue number2
DOIs
Publication statusPublished - 2010

Fingerprint

Multi agent systems
Specifications
Agglomeration
Model checking

Cite this

@article{b7e42b55e8864e499cd0a4d3fec3e409,
title = "Automated Analysis of Compositional Multi-Agent Systems",
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. Copyright {\circledC} 2010 Inderscience Enterprises Ltd.",
author = "O. Sharpanskykh and J. Treur",
year = "2010",
doi = "10.1504/ijaose.2010.032801",
language = "English",
volume = "4",
pages = "174--221",
journal = "International Journal of Agent-Oriented Software Engineering",
issn = "1746-1375",
publisher = "Inderscience Enterprises Ltd",
number = "2",

}

Automated Analysis of Compositional Multi-Agent Systems. / Sharpanskykh, O.; Treur, J.

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

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Automated Analysis of Compositional Multi-Agent Systems

AU - Sharpanskykh, O.

AU - Treur, J.

PY - 2010

Y1 - 2010

N2 - 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. Copyright © 2010 Inderscience Enterprises Ltd.

AB - 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. Copyright © 2010 Inderscience Enterprises Ltd.

U2 - 10.1504/ijaose.2010.032801

DO - 10.1504/ijaose.2010.032801

M3 - Article

VL - 4

SP - 174

EP - 221

JO - International Journal of Agent-Oriented Software Engineering

JF - International Journal of Agent-Oriented Software Engineering

SN - 1746-1375

IS - 2

ER -