Model Checking for ACL Compliance Verification


Marc-Philippe Huget, Michael J. Wooldridge

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

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.

 @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:

Pubblicazione

— autori/autrici

Marc-Philippe Huget, Michael J. Wooldridge

— a cura di

Frank Dignum

— stato

pubblicato

— tipo

capitolo di libro

Sede di pubblicazione

— volume

Advances in Agent Communication

— volume

2922

— pagine

75-90

— data di pubblicazione

2004

URL

pagina originale  |  PDF originale

Identificatori

— 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-2022 APICe@DISI Research Group - PRIVACY