Verifying multi-agent programs by model checking

Bordini, Rafael H.; Fisher, Michael; Visser, Willem; Wooldridge, Michael

Abstract

This paper gives an overview of our recent work on an approach to verifying multi-agent programs. We automatically translate multi-agent systems programmed in the logic-based agent-oriented programming language AgentSpeak into either Promela or Java, and then use the associated Spin and JPF model checkers to verify the resulting systems. We also describe the simplified BDI logical language that is used to write the properties we want the systems to satisfy. The approach is illustrated by means of a simple case study.

Citation

Bordini, R. H., Fisher, M., Visser, W., & Wooldridge, M. (2006). Verifying multi-agent programs by model checking. Autonomous Agents and Multi-Agent Systems, 12(2), 239-256. https://doi.org/10.1007/s10458-006-5955-7

• Journal Article Type: Article
• Publication Date: 2006-03
• Deposit Date: Apr 23, 2008
• Journal: Autonomous Agents and Multi-Agent Systems
• Print ISSN: 1387-2532
• Electronic ISSN: 1573-7454
• Publisher: Springer
• Peer Reviewed: Peer Reviewed
• Volume: 12
• Issue: 2
• Pages: 239-256
• DOI: https://doi.org/10.1007/s10458-006-5955-7
• Keywords: Agent-oriented programming, AgentSpeak, Model checking, Spin, JPF.
• Public URL: https://durham-repository.worktribe.com/output/1558637
• Publisher URL: http://www.springerlink.com/openurl.asp?genre=article&eissn=1573-7454&volume=12&issue=2&spage=239