Compositional Verification of a Multi-Agent System for One-to-Many Negotiation

F.M. Brazier, F.J. Cornelissen, R. Gustavsson, C.M. Jonker, O. Lindeberg, B. Polak, J. Treur

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

Verification of multi-agent systems hardly occurs in design practice. One of the difficulties is that required properties for a multi-agent system usually refer to multi-agent behaviour which has nontrivial dynamics. To constrain these multi-agent behavioural dynamics, often a form of organisational structure is used, for example, for negotiating agents, by following strict protocols. The claim is that these negotiation protocols entail a structured process that is manageable with respect to analysis, design and execution of such a multi-agent system. In this paper this is shown by a case study: verification of a multi-agent system for one-to-many negotiation in the domain of load balancing of electricity use. A compositional verification method for multi-agent systems is applied that allows to (1) logically relate dynamic properties of the multi-agent system as a whole to dynamic properties of agents, and (2) logically relate dynamic properties of agents to properties of their subcomponents. Given that properties of these subcomponents can be verified by more standard methods, these logical relationships provide proofs of the dynamic properties of the multi-agent system as a whole.
Original languageEnglish
Pages (from-to)95-117
JournalApplied Intelligence
Volume20
Issue number2
DOIs
Publication statusPublished - 2004

Fingerprint

Multi agent systems
Network protocols
Resource allocation
Electricity

Bibliographical note

Brazier.ea:04

Cite this

Brazier, F. M., Cornelissen, F. J., Gustavsson, R., Jonker, C. M., Lindeberg, O., Polak, B., & Treur, J. (2004). Compositional Verification of a Multi-Agent System for One-to-Many Negotiation. Applied Intelligence, 20(2), 95-117. https://doi.org/10.1023/B:APIN.0000013334.33853.0c
Brazier, F.M. ; Cornelissen, F.J. ; Gustavsson, R. ; Jonker, C.M. ; Lindeberg, O. ; Polak, B. ; Treur, J. / Compositional Verification of a Multi-Agent System for One-to-Many Negotiation. In: Applied Intelligence. 2004 ; Vol. 20, No. 2. pp. 95-117.
@article{5b5eead083304df38b650c9973ac0dc0,
title = "Compositional Verification of a Multi-Agent System for One-to-Many Negotiation",
abstract = "Verification of multi-agent systems hardly occurs in design practice. One of the difficulties is that required properties for a multi-agent system usually refer to multi-agent behaviour which has nontrivial dynamics. To constrain these multi-agent behavioural dynamics, often a form of organisational structure is used, for example, for negotiating agents, by following strict protocols. The claim is that these negotiation protocols entail a structured process that is manageable with respect to analysis, design and execution of such a multi-agent system. In this paper this is shown by a case study: verification of a multi-agent system for one-to-many negotiation in the domain of load balancing of electricity use. A compositional verification method for multi-agent systems is applied that allows to (1) logically relate dynamic properties of the multi-agent system as a whole to dynamic properties of agents, and (2) logically relate dynamic properties of agents to properties of their subcomponents. Given that properties of these subcomponents can be verified by more standard methods, these logical relationships provide proofs of the dynamic properties of the multi-agent system as a whole.",
author = "F.M. Brazier and F.J. Cornelissen and R. Gustavsson and C.M. Jonker and O. Lindeberg and B. Polak and J. Treur",
note = "Brazier.ea:04",
year = "2004",
doi = "10.1023/B:APIN.0000013334.33853.0c",
language = "English",
volume = "20",
pages = "95--117",
journal = "Applied Intelligence",
issn = "0924-669X",
publisher = "Springer Verlag",
number = "2",

}

Brazier, FM, Cornelissen, FJ, Gustavsson, R, Jonker, CM, Lindeberg, O, Polak, B & Treur, J 2004, 'Compositional Verification of a Multi-Agent System for One-to-Many Negotiation' Applied Intelligence, vol. 20, no. 2, pp. 95-117. https://doi.org/10.1023/B:APIN.0000013334.33853.0c

Compositional Verification of a Multi-Agent System for One-to-Many Negotiation. / Brazier, F.M.; Cornelissen, F.J.; Gustavsson, R.; Jonker, C.M.; Lindeberg, O.; Polak, B.; Treur, J.

In: Applied Intelligence, Vol. 20, No. 2, 2004, p. 95-117.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Compositional Verification of a Multi-Agent System for One-to-Many Negotiation

AU - Brazier, F.M.

AU - Cornelissen, F.J.

AU - Gustavsson, R.

AU - Jonker, C.M.

AU - Lindeberg, O.

AU - Polak, B.

AU - Treur, J.

N1 - Brazier.ea:04

PY - 2004

Y1 - 2004

N2 - Verification of multi-agent systems hardly occurs in design practice. One of the difficulties is that required properties for a multi-agent system usually refer to multi-agent behaviour which has nontrivial dynamics. To constrain these multi-agent behavioural dynamics, often a form of organisational structure is used, for example, for negotiating agents, by following strict protocols. The claim is that these negotiation protocols entail a structured process that is manageable with respect to analysis, design and execution of such a multi-agent system. In this paper this is shown by a case study: verification of a multi-agent system for one-to-many negotiation in the domain of load balancing of electricity use. A compositional verification method for multi-agent systems is applied that allows to (1) logically relate dynamic properties of the multi-agent system as a whole to dynamic properties of agents, and (2) logically relate dynamic properties of agents to properties of their subcomponents. Given that properties of these subcomponents can be verified by more standard methods, these logical relationships provide proofs of the dynamic properties of the multi-agent system as a whole.

AB - Verification of multi-agent systems hardly occurs in design practice. One of the difficulties is that required properties for a multi-agent system usually refer to multi-agent behaviour which has nontrivial dynamics. To constrain these multi-agent behavioural dynamics, often a form of organisational structure is used, for example, for negotiating agents, by following strict protocols. The claim is that these negotiation protocols entail a structured process that is manageable with respect to analysis, design and execution of such a multi-agent system. In this paper this is shown by a case study: verification of a multi-agent system for one-to-many negotiation in the domain of load balancing of electricity use. A compositional verification method for multi-agent systems is applied that allows to (1) logically relate dynamic properties of the multi-agent system as a whole to dynamic properties of agents, and (2) logically relate dynamic properties of agents to properties of their subcomponents. Given that properties of these subcomponents can be verified by more standard methods, these logical relationships provide proofs of the dynamic properties of the multi-agent system as a whole.

U2 - 10.1023/B:APIN.0000013334.33853.0c

DO - 10.1023/B:APIN.0000013334.33853.0c

M3 - Article

VL - 20

SP - 95

EP - 117

JO - Applied Intelligence

JF - Applied Intelligence

SN - 0924-669X

IS - 2

ER -

Brazier FM, Cornelissen FJ, Gustavsson R, Jonker CM, Lindeberg O, Polak B et al. Compositional Verification of a Multi-Agent System for One-to-Many Negotiation. Applied Intelligence. 2004;20(2):95-117. https://doi.org/10.1023/B:APIN.0000013334.33853.0c