Title: Formal specification and validation of multi-agent behaviour using TLA+ and TLC model checker

Authors: Toufik Taibi

Addresses: Department of Electrical and Computer Engineering, University of Western Ontario, London, Ontario N6A 5B9, Canada

Abstract: This work views agent coordination from a purely behavioural viewpoint. We use the Temporal Logic of Actions (TLA) to formally specify the behaviour of individual agents as well as the behaviour of a coalition of agents by composing the behaviour of individual agents. We view a coalition of agents as being initiated by an agent wishing to delegate some of its tasks to others. We do not discuss the issues related to coalition formation here but rather focus on how agent coordination can be achieved through behaviour composition. We have built a generic and rigorous approach to formally specify such behaviour composition from the behaviour of individual agents. To validate our approach, we have successfully applied it to the blocks world and model checked the specifications using TLC – the TLA model checker.

Keywords: TLA; temporal logic of actions; TLA+; behaviour composition; coalition; model checking; TLC; agent coordination; multi-agent systems; MAS; agent-based systems; software agents.

DOI: 10.1504/IJAISC.2008.021266

International Journal of Artificial Intelligence and Soft Computing, 2008 Vol.1 No.1, pp.99 - 113

Published online: 14 Nov 2008 *

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