| 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.
|
 Additional Information
|
Citation:
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge,
"State-Space Reduction Techniques in Agent Verification,"
aamas,
pp. 896-903,
Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 2 (AAMAS'04),
2004
|
