Title: Deadlock verification of a DPS coordination strategy and its alternative model in pi-calculus

Authors: Pablo D. Robles-Granda; Elham S. Khorasani; Shahram Rahimi; Norman Carver

Addresses: Department of Computer Science, Southern Illinois University, Carbondale, 62901, USA. ' Department of Computer Science, Southern Illinois University, Carbondale, 62901, USA. ' Department of Computer Science, Southern Illinois University, Carbondale, 62901, USA. ' Department of Computer Science, Southern Illinois University, Carbondale, 62901, USA

Abstract: A key issue for distributed problem solving (DPS) systems is coordination of the agent's actions, and methods for producing effective coordination strategies remain an active area of research. Because there are not yet approaches that can automatically produce such strategies, some human engineering is often still necessary. As a result, there is a need for a formal tool to support such human engineering. In a previous work (Khorasani et al., 2009), we investigated the use of pi-calculus as a formal language for modelling DPS coordination strategies and showed how such models could be used to evaluate the time performance of a strategy. In this paper, we focus on verification of coordination strategies. More specifically, we utilise the formal semantics of pi-calculus to detect deadlocks in a coordination strategy. We also show how, by imposing certain constraints on the pi-calculus model, one would be able to design a deadlock-free coordination strategy.

Keywords: pi-calculus; distributed problem solving; DPS; coordination strategies; multi-agent systems; MAS; agent-based systems; modelling; deadlock verification; deadlock detection.

DOI: 10.1504/IJIIDS.2012.045847

International Journal of Intelligent Information and Database Systems, 2012 Vol.6 No.2, pp.154 - 179

Received: 25 Aug 2010
Accepted: 30 Jan 2011

Published online: 16 Aug 2014 *

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