Model Checking Commitment Protocols

8 years 9 months ago
Model Checking Commitment Protocols
Using model checking to verify that interaction protocols have given properties is widely recognized as an important issue in multiagent systems where autonomous and heterogeneous agents need to successfully regulate and coordinate their interactions. In this paper, we investigate the use of symbolic model checkers to verify the compliance of a special kind of interaction protocols called commitment protocols with some properties such as liveness and safety. These properties are expressed as formulae in a new temporal logic, called CTLC, which extends the temporal logic CTL with modality for social commitments. Our approach shows that the problem of model checking CTLC can be reduced to the problem of model checking either CTLK or ARCTL, which are extensions of CTL. We finally present an implementation and report on the experimental results of verifying the Contract Net Protocol modeled in terms of commitments and associated actions using the symbolic model checkers MCMAS and extended...
Mohamed El-Menshawy, Jamal Bentahar, Rachida Dssou
Added 29 Aug 2011
Updated 29 Aug 2011
Type Journal
Year 2011
Authors Mohamed El-Menshawy, Jamal Bentahar, Rachida Dssouli
Comments (0)