Automatic Verification of Communicative Commitments using Reduction
Mofleh Al-diabat, Faisal Al-saqqar, Ashraf Al-saqqar
Journal of Intelligent Computing, Vol. 9, No. 3, 2018.
DOI: 
Link: http://www.dline.info/jic/fulltext/v9n3/jicv9n3_3.pdf
Abstract:
Albeit the 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 communication and fulfillment of commitments. 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 CTL com 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.