Model Checking for PRS-Like Agents

The key problem in applying verification techniques such as model checking to agent architectures is to show how to map systematically from an agent program to a model structure that not only includes the possible behaviours of the agent in its environment, but which also captures appropriate mental notions, such as belief, desire and intention, that may be used by the designer to reason about the agent. In this paper, we present an algorithm providing a mapping from agent programs under a simplified PRS-type agent architecture to a reachability graph structure extended to include representations of beliefs, goals and intentions, and illustrate the translation with a simple “waypoint following” agent. We conclude with a brief discussion of the differences between the internal (operational) notion of intention used in the architecture and the formal (external) notion of intention used in the modelling.

• Type: Conference
• Year: 2005
• Where: AUSAI
• Authors: Wayne Wobcke, Marc Chee, Krystian Ji
• Keywords: Agent Architecture, Agent Programs, Artificial Intelligence, AUSAI 2005, Simplified Prs-type Agent