Automatic Verification of Communicative Commitments using Reduction

Abstract

In spite of the fact that modeling and verification of the Multi-Agent Systems (MASs) have been since long under study, there are several related challenges that should still be addressed. In effect, several frameworks have been established for modeling and verifying the MASs with regard to communicative commitments. A bulky volume of research has been conducted for defining semantics of these systems. Though, formal verification of these systems is still unresolved research problem. Within this context, this paper presents the CTL^com that reforms the CTLC, i.e., the temporal logic of the commitments, so as to enable reasoning about the commitments and fulfillment.  Moreover, the paper introduces a fully-automated method for verification of the logic by means of trimming down the problem of a model that checks the CTLcom to a problem of a model that checks the GCTL*, which is a generalized version of the CTL* with action formulae. By so doing, we take advantage of the CWB-NC automata-based model checker as a tool for verification. Lastly, this paper presents a case study drawn from the business field, that is, the NetBill protocol, illustrates its implementation, and discusses the associated experimental results in order to illustrate the efficiency and effectiveness of the suggested technique.

Keywords: Multi-Agent Systems, Model Checking, Communicative commitment's, Reduction.