Automatic Verification of Communicative Commitments using Reduction

Mofleh Al-Diabat, Faisal Al-Saqqar, Ashraf Al-Saggar


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

Full Text: PDF
Download the IISTE publication guideline!

To list your conference here. Please contact the administrator of this platform.

Paper submission email:
ISSN (Paper)2224-5782 ISSN (Online)2225-0506
Please add our address "" into your email contact list.
This journal follows ISO 9001 management standard and licensed under a Creative Commons Attribution 3.0 License.
Copyright ©