Formal description and verification of MAS interaction protocols

Issue title: Special Issue on Agent-oriented Software Development Methodologies

Guest editors: Hong Zhu

Article type: Research Article

Authors: Chen, Hongbing^a | Yang, Qun^a | Li, Qianmu^{a; b} | Xu, Manwu^{a; *}

Affiliations: [a] State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China | [b] Department of Computer Science and Technology, Nanjing University of Science and Technology, Nanjing 210094, China | Department of Computing, Oxford Brookes University, Oxford OX33 1HX, UK

Correspondence: [*] Corresponding author: Xu Manwu, Department of Computer Science and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, 210093. Tel.: +86 025 51562673; E-mail: [email protected]

Abstract: Formal description and verification of interaction protocols is an important field of MAS. In this paper a calculus for describing interaction protocols of MAS is defined. The calculus is based on process algebra and is independent of any particular model of rational agency. This makes it applicable to verify the protocol of heterogeneous agent systems. With the formal semantics of calculus, some properties of session protocols, e.g. termination, deadlock, can be verified. The approach can avoid the problem of semantic verification, because the states of the protocol are defined in the protocol itself. The formal interaction protocol specifies the complex concurrent and asynchronous pattern of communication between agents and can be verified straightforward that whether an agent acts in accordance with the protocol or not.

Keywords: Interaction protocol, multi-agent, π-calculus

DOI: 10.3233/MGS-2006-2404

Journal: Multiagent and Grid Systems, vol. 2, no. 4, pp. 353-363, 2006