APICe » Publications » Bordini03

Model Checking AgentSpeak

Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael J. Wooldridge
This paper introduces AgentSpeak(F), a variation of the BDI logic programming language AgentSpeak(L) intended to permit the model-theoretic verification of multi-agent systems. After briefly introducing AgentSpeak(F) and discussing its relationship to AgentSpeak(L), we show how AgentSpeak(F) programs can be transformed into Promela, the model specification language for the Spin model-checking system. We also describe how specifications written in a simplified form of BDI logic can be transformed into Spin-format linear temporal logic formul. With our approach, it is thus possible to automatically verify whether or not multi-agent systems implemented in AgentSpeak(F) satisfy specifications expressed as BDI logic formul. We illustrate our approach with a short case study, in which we show how BDI properties of a simulated auction system implemented in AgentSpeak(F) were verified.
Keywords: AgentSpeak(F), AgentSpeak(L), BDI Logic, Multiagent Systems
Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-Agents Systems, 2003
@article{bordini03,
 Author = {Bordini, Rafael H. and Fisher, Michael and Pardavila, Carmen and Wooldridge, Michael J.},
 Journal = {Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-Agents Systems},
 Title = {Model Checking AgentSpeak},
 Year = 2003
}