Marc-Philippe Huget, Michael J. Wooldridge

The problem of checking that agents correctly implement the semantics of an agent communication language has become increasingly important as agent technology makes its transition from the research laboratory to field-tested applications. In this paper, we show how model checking techniques can be applied to this problem. Model checking is a technique developed within the formal methods community for automatically verifying that finite-state concurrent systems implement temporal logic specifications. We first describe a variation of the MABLE multiagent bdi programming language, which permits the semantics (pre- and post-conditions) of acl performatives to be defined separately from a system where these semantics are used. We then show how assertions defining compliance to the semantics of an acl can be captured as claims about MABLE agents, expressed using MABLE’s associated assertion language. In this way, compliance to acl semantics reduces to a conventional model checking problem. We illustrate our approach with a number of short case studies.

Advances in Agent Communication, pages 75-90,  2004.
Frank Dignum (eds.), Springer.
International Workshop on Agent Communication Languages (ACL 2003), Melbourne, Australia, 14 July 2003. Revised and Invited Papers

@incollection{modelcheckingacl-acl03,
Author = {Huget, Marc-Philippe and Wooldridge, Michael J.},
Booktitle = {Advances in Agent Communication},
Doi = {10.1007/978-3-540-24608-4_5},
Editor = {Dignum, Frank},
Isbn = {978-3-540-20769-6},
Note = {International Workshop on Agent Communication Languages (ACL 2003), Melbourne, Australia, 14~} # jul # {~2003. Revised and Invited Papers},
Pages = {75--90},
Publisher = {Springer},
Title = {Model Checking for {ACL} Compliance Verification},
Url = {http://www.springerlink.com/content/8d2rqhdyfjj4klnd/},
Volume = 2922,
Year = 2004}
Tags:

Publication

— authors

Marc-Philippe Huget, Michael J. Wooldridge

— editors

Frank Dignum

— status

published

— sort

book chapter

Venue

— volume

Advances in Agent Communication

— volume

2922

— pages

75-90

— publication date

2004

URLs

original page  |  original PDF

Identifiers

— DOI

10.1007/978-3-540-24608-4_5

— print ISBN

978-3-540-20769-6

BibTeX

— BibTeX ID
modelcheckingacl-acl03
— BibTeX category
incollection

Partita IVA: 01131710376 - Copyright © 2008-2021 APICe@DISI Research Group - PRIVACY