@inproceedings{f8b9be98e3fc4711af8dd4f2f3718e90,
title = "A new model checking approach for verifying agent communication protocols",
abstract = "In this paper, we propose a new model checking algorithm for verifying dialogue game protocols (DGP) for multi-agent communication. These protocols are specified as transition systems in which transitions are labeled with communicative acts. Our underlying logic (SCCTL*) used to specify the properties to be verified extends CTL* by adding action formulae, the actions we deal with are actions that agents perform on social commitments when communicating. The verification method is based on the translation of SCCTL* formulae into a variant of alternating tree automata called Alternating B{\"u}chi Tableau Automata (ABTA). Our algorithm explores the product graph of the protocol and the ABTA representing the formula to be verified. The nodes of the product graph are signed according to the type of the formula (with or without negation). We propose a set of tableau inference rules for specifying the translation procedure. The efficiency of our algorithm is due to the fact that it uses only one depth-first search instead of two. Our algorithm explores directly the product graph using the sign of the nodes. This algorithm is an on-the-fly efficient algorithm.",
keywords = "Model checking, Multi-agent communication, Temporal logic",
author = "Jamal Bentahar and Bernard Moulin and Meyer, {John Jules Ch}",
year = "2006",
doi = "10.1109/CCECE.2006.277640",
language = "British English",
isbn = "1424400384",
series = "Canadian Conference on Electrical and Computer Engineering",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1586--1590",
booktitle = "2006 Canadian Conference on Electrical and Computer Engineering, CCECE'06",
address = "United States",
note = "2006 Canadian Conference on Electrical and Computer Engineering, CCECE'06 ; Conference date: 07-05-2006 Through 10-05-2006",
}