Property-based slicing for agent verification
Date
2009-12
Authors
Bordini, Rafael H.
Fisher, Michael
Wooldridge, Michael
Visser, Willem
Journal Title
Journal ISSN
Volume Title
Publisher
Oxford University Press (OUP)
Abstract
Programming languages designed specifically for multi-agent systems represent a new programming paradigm that has
gained popularity over recent years, with some multi-agent programming languages being used in increasingly sophisticated
applications, often in critical areas. To support this, we have developed a set of tools to allow the use of model-checking
techniques in the verification of systems directly implemented in one particular language called AgentSpeak. The success
of model checking as a verification technique for large software systems is dependent partly on its use in combination with
various state-space reduction techniques, an important example of which is property-based slicing. This article introduces an
algorithm for property-based slicing of AgentSpeak multi-agent systems. The algorithm uses literal dependence graphs, as
developed for slicing logic programs, and generates a program slice whose state space is stuttering-equivalent to that of the
original program; the slicing criterion is a property in a logic with LTL operators and (shallow) BDI modalities. In addition
to showing correctness and characterizing the complexity of the slicing algorithm, we apply it to an AgentSpeak program
based on autonomous planetary exploration rovers, and we discuss how slicing reduces the model-checking state space. The
experiment results show a significant reduction in the state space required for model checking that agent, thus indicating that
this approach can have an important impact on the future practicality of agent verification.
Description
The original publication is available at http://logcom.oxfordjournals.org/
Keywords
Intelligent agents (Computer software), Multiagent systems, Computer programming
Citation
Bordini, R.H., Fisher, M., Wooldridge, M. & Visser, W. 2009. Property-based slicing for agent verification. Journal of Logic and Computation, 9(6):1385-1425, doi:10.1093/logcom/exp029.