Model checking communicative agent-based systems

Jamal Bentahar; John Jules Meyer

Model checking communicative agent-based systems

Jamal Bentahar, John Jules Meyer

Electrical Engineering

Utrecht University

Research output: Contribution to conference › Paper › peer-review

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.

Original language	British English
State	Published - 2007
Event	6th International Conference on Software Methodologies, Tools and Techniques, SoMeT_07 - Rome, Italy Duration: 7 Nov 2007 → 9 Nov 2007

Conference

Conference	6th International Conference on Software Methodologies, Tools and Techniques, SoMeT_07
Country/Territory	Italy
City	Rome
Period	7/11/07 → 9/11/07

Keywords

Model checking
Multi-agent systems
Temporal logic

Cite this

@conference{fc214060a67b44a298759a02005a1bb4,

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 editors and anonymous reviewers for their valuable comments and helpful suggestions for improvements. We also thank the Natural Sciences and Engineering Research Council of Canada (NSERC), le Fond Qu{\'e}b{\'e}cois de la Recherche sur la Nature et les Technologies (NATEQ) and Concordia University (seed funding) for their financial support. ; 6th International Conference on Software Methodologies, Tools and Techniques, SoMeT_07 ; Conference date: 07-11-2007 Through 09-11-2007",

year = "2007",

language = "British English",

}

TY - CONF

T1 - Model checking communicative agent-based systems

AU - Bentahar, Jamal

AU - Meyer, John Jules

N1 - Funding Information: We would like to thank the editors and anonymous reviewers for their valuable comments and helpful suggestions for improvements. We also thank the Natural Sciences and Engineering Research Council of Canada (NSERC), le Fond Québécois de la Recherche sur la Nature et les Technologies (NATEQ) and Concordia University (seed funding) for their financial support.

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - Model checking

KW - Multi-agent systems

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?scp=84863413049&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:84863413049

T2 - 6th International Conference on Software Methodologies, Tools and Techniques, SoMeT_07

Y2 - 7 November 2007 through 9 November 2007

ER -

Model checking communicative agent-based systems

Abstract

Conference

Keywords

Other files and links

Fingerprint

Cite this