APICe » Publications » ModelcheckingaclAcl2003

Model Checking for ACL Compliance Verification

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}