| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 405360 | Knowledge-Based Systems | 2009 | 18 Pages |
Abstract
Model checking is a formal technique used to verify communication protocols against given properties. In this paper, we propose a new model checking algorithm aims at verifying systems designed as a set of autonomous interacting agents. These software agents are equipped with knowledge and beliefs and interact with each other according to protocols governed by a set of logical rules. We present a tableauased version of this algorithm and provide the soundness, completeness, termination and complexity results. A case study about an agent-based negotiation protocol and its implementation are also described.
Related Topics
Physical Sciences and Engineering
Computer Science
Artificial Intelligence
Authors
Jamal Bentahar, John-Jules Meyer, Wei Wan,