@inproceedings{65f92055be4948f39d7381fde638048a,
title = "Model Checking Communicative Agent-Based Systems",
abstract = "Model checking is a formal technique used to verify communication protocols against given properties. In this paper, we address the problem of verifying systems designed as a set of autonomous interacting agents using such a technique. 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 tableau-based model checking algorithm for these systems and provide the termination and complexity results.",
keywords = "model checking, Multi-agent systems, temporal logic",
author = "Jamal Bentahar and Meyer, {John Jules}",
note = "Funding Information: We would like to thank the Natural Sciences and Engineering Research Council of Canada (NSERC) and le Fond Qu{\'e}b{\'e}cois de la Recherche sur la Nature et les Technologies (NATEQ) for their financial support. We are also grateful to the editors and the four reviewers for their valuable comments which helped us to improve the quality of the paper. Publisher Copyright: {\textcopyright} 2010 The authors and IOS Press. All rights reserved.; 6th International Conference on New Trends in Software Methodology Tools, and Techniques, SoMeT 2007 ; Conference date: 07-11-2007 Through 09-11-2007",
year = "2007",
language = "British English",
series = "Frontiers in Artificial Intelligence and Applications",
publisher = "IOS Press BV",
pages = "239--265",
editor = "Hamido Fujita and Domenico Pisanelli",
booktitle = "New Trends in Software Methodologies, Tools and Techniques",
address = "Netherlands",
}