Model checking agentspeak
- 14 July 2003
- proceedings article
- Published by Association for Computing Machinery (ACM)
- p. 409-416
- https://doi.org/10.1145/860575.860641
Abstract
This paper introduces ASF, a variation of the BDI logic programming language ASL intended to permit the model-theoretic verification of multi-agent systems. After briefly introducing ASF and discussing its relationship to ASL, we show how ASF programs can be transformed into Prm, 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 formulae. With our approach, it is thus possible to automatically verify whether or not multi-agent systems implemented in ASF 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 ASF were verified.Keywords
This publication has 8 references indexed in Scilit:
- AgentSpeak(XL)Published by Association for Computing Machinery (ACM) ,2002
- Model checking multi-agent systems with MABLEPublished by Association for Computing Machinery (ACM) ,2002
- Formal analysis of a space-craft controller using SPINIEEE Transactions on Software Engineering, 2001
- Reasoning about Rational AgentsPublished by MIT Press ,2000
- Remote Agent: to boldly go where no AI system has gone beforeArtificial Intelligence, 1998
- Engineering AgentSpeak(L): a formal computational modelJournal of Logic and Computation, 1998
- Decision procedures for BDI logicsJournal of Logic and Computation, 1998
- The model checker SPINIEEE Transactions on Software Engineering, 1997