A tableau method for verifying dialogue game protocols for agent communication

In this paper, we propose a new tableau-based model checking technique for verifying dialogue game protocols for agent communication. These protocols are defined using our social commitment-based framework for agent communication called Commitment and Argument Network (CAN). We use a variant of CTL* (ACTL*) for specifying these protocols and the properties to be verified. This logic extends CTL* by allowing formulae to constrain actions as well as states. The verification method is based on the translation of formulae into a variant of alternating tree automata called Alternating Büchi Tableau Automata (ABTA). We propose a set of tableau rules (inference rules) for specifying this translation procedure. Unlike the model checking algorithms proposed in the literature, the algorithm that we propose in this paper allows us not only to verify if the dialogue game protocol (the model) satisfies a given property, but also if this protocol respects the tableau rules-based decomposition of the action formulae. This algorithm is an on-the-fly efficient algorithm.