Model Checking Commitment Protocols
Mohamed El-Menshawy, Jamal Bentahar, Rachida Dssouli · 2011
Abstract. We investigate the problem of verifying commitment protocols that are widely used to regulate interactions among cognitive agents by means of model checking. We present a new logic-based language to specify commitment protocols, which is derived from extending CTL ∗ with modalities for social commitments and associated actions. We report on the implementation of the NetBill protocol—a motivated and specified example in the proposed language—using three model checkers (MCMAS, NuSMV, and CWB-NC) and compare the experimental results obtained. 1