State-Space Reduction Techniques in Agent Verification

We have developed a set of tools to allow the use of model-checking techniques for the verification of systems directly implemented in an agent-oriented programming language. The success of model checking as a verification technique for large systems is dependent partly on its use in combination with various state-space reduction techniques. An important example of such techniques is property-based slicing. This paper introduces an algorithm for propertybased slicing of AgentSpeak multi-agent systems. We apply our approach to the AgentSpeak code for a scenario inspired by routine tasks of autonomous Mars rovers, and explain how slicing reduces the search space in theory. We consider experiments on such scenarios, and initial results show a significant reduction in the state space, thus indicating that this approach can have an important impact on the practicality of agent verification.

• Type: Conference
• Year: 2004
• Where: ATAL
• Authors: Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge
• Keywords: Agent-oriented Programming Language, AgentSpeak Multi-agent Systems, ATAL 2004, Intelligent Agents, State-space Reduction Techniques