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.
Verifiable Multi-agent Programs
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael J. Wooldridge
Mehdi M. Dastani, Jürgen Dix, Amal El Fallah-Seghrouchni (eds.)
Programming Multi-agent Systems, pages 72–89
Lecture Notes in Computer Science 3067
Springer
2004
AgentSpeak is a reactive planning language for programming autonomous agents. It has recently been shown that model checking techniques can be applied to the verification of AgentSpeak systems, through a translation to Promela, the model specification language for the SPIN LTL model-checking system. In this paper, we introduce an alternative verification approach for AgentSpeak, by translating AgentSpeak to Java and then applying JPF2, a general purpose Java model checker. The primary advantage of this approach is that Java is the language of choice for most agent implementations, and the approach is thus much closer to the current practice of agent development than the Promela-based approach. Also, models of AgentSpeak agents represented in Java are both clearer and more natural than those given in Promela. We examine both alternatives by means of a practical application, provide a qualitative comparison between them, and identify some key issues for future research.
PROMAS 2003 @ AAMAS 2003
Programming Multi-Agent Systems (edited volume, 2004) — Mehdi Dastani, Jürgen Dix, Amal El Fallah Seghrouchni