State-space reduction techniques in agent verification.

Abstract

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.