Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 2 (AAMAS'04)
State-Space Reduction Techniques in Agent Verification
New York City, New York, USA
July 19-July 23
ISBN: 0-7695-2092-8
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 property-based 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.
Citation:
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge, "State-Space Reduction Techniques in Agent Verification," aamas, vol. 2, pp.896-903, Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 2 (AAMAS'04), 2004