id: 05887454
dt: a
an: 05887454
au: El-Menshawy, Mohamed; Bentahar, Jamal; Dssouli, Rachida
ti: Symbolic model checking commitment protocols using reduction.
so: Omicini, Andrea (ed.) et al., Declarative agent languages and technologies
    VIII. 8th international workshop, DALT 2010, Toronto, Canada, May 10,
    2010. Revised, selected and invited papers. Berlin: Springer (ISBN
    978-3-642-20714-3/pbk). Lecture Notes in Computer Science 6619, 185-203
    (2011).
py: 2011
pu: Berlin: Springer
la: EN
cc: 
ut: multi-agent systems; commitment protocols; symbolic model checking;
    protocol properties
ci: 
li: doi:10.1007/978-3-642-20715-0_11
ab: Summary: Using model checking to verify that interaction protocols have
    given properties is widely recognized as an important issue in
    multi-agent 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 NuSMV.
rv: