Verifying conformance of multi-agent commitment-based protocols |
| |
Authors: | Mohamed El-Menshawy Jamal Bentahar Warda El Kholy Rachida Dssouli |
| |
Affiliation: | Concordia University, Concordia Institute for Information Systems Engineering 1515 Ste-Catherine Street West, EV. 640, Montreal, Quebec, Canada H3G 2W1 |
| |
Abstract: | Although several approaches have been proposed to specify multi-agent commitment-based protocols that capture flexible and rich interactions among autonomous and heterogeneous agents, very few of them synthesize their formal specification and automatic verification in an integrated framework. In this paper, we present a new logic-based language to specify commitment-based protocols, which is derived from ACTL1c, a logic extending CTL1 with modalities to represent and reason about social commitments and their actions. We present a reduction technique that formally transforms the problem of model checking ACTL1c to the problem of model checking GCTL1 (an extension of CTL1 with action formulae). We prove that the reduction technique is sound and we fully implement it on top of the CWB-NC model checker to automatically verify the NetBill protocol, a motivated and specified example in the proposed specification language. We also apply the proposed technique to check the compliance of another protocol: the Contract Net protocol with given properties and report and discuss the obtained results. We finally develop a new symbolic algorithm to perform model checking dedicated to the proposed logic. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|