Skip Navigation



Journal of Logic and Computation Advance Access published online on June 16, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp029
This Article
Right arrow Full Text (PDF)
Right arrow References
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bordini, R. H.
Right arrow Articles by Visser, W.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Property-based Slicing for Agent Verification

Rafael H. Bordini

Department of Computer Science, University of Durham, Durham, UK.
E-mail: R.Bordini{at}inf.ufrgs.br
Present Address: Institute of Informatics, Federal University of Rio Grande do Sul, Porto Alegre, Brazil.

Michael Fisher and Michael Wooldridge

Department of Computer Science, University of Liverpool, Liverpool, UK.
E-mail: MFisher{at}liverpool.ac.uk; mjw{at}liverpool.ac.uk

Willem Visser

Department of Mathematical Sciences, Computer Science Division, Stellenbosch University, Stellenbosch, South Africa.
E-mail: wvisser{at}cs.sun.ac.za

Received 1 May 2009.


  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.

Keywords: Program verification; multi-agent programming languages; property-based slicing; model checking; multi-agent systems


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.