Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael J. Wooldridge
Jeffrey S. Rosenschein, Michael J. Wooldridge, Tuomas Sandholm, Makoto Yokoo (eds.)
2nd International Joint Conference on Autonomous Agents and Multi-Agents Systems (AAMAS 2003), pages 409-416
ACM Press, New York, NY, USA
11-14 July 2003
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 |
