Enter a brief description of your changes
(Required)
Minor changes are by default collapsed in the page history.
No changes
The page does not exist yet.
Failed to load changes
Version by on
Leave Collaboration
Are you sure you want to leave the realtime collaboration and continue editing alone? The changes you save while editing alone will lead to merge conflicts with the changes auto-saved by the realtime editing session.
Model Checking AgentSpeak
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.
keywordsAgentSpeak(F), AgentSpeak(L), BDI Logic, Multiagent Systems
The Second International Joint Conference on Autonomous Agents & Multiagent Systems (edited volume, 2003) —