A New Model Checking Approach for Verifying Agent Communication Protocols

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 Buchi 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