Symbolic Model Checking for Agent Interactions

In this paper, we address the issue of the specification andverification of commitment protocols having a social semantics. We begin with developing a new language to formallyspecify these protocols and desirable properties by enhancing $CTL^*$ logic with modalities of commitments and actions on these commitments. We also present a symbolicmodel checking algorithm for commitments and their actions based on OBDDs. Finally, we present an implementation and experimental results of the proposed protocol usingthe NuSMV and MCMAS symbolic model checkers.

Authors

• Mohamed El-Menshawy
• Wei Wan National Engineering Research Center for Big Data Technology and System Services Computing Technology and System Lab Hubei Engineering Research Center on Big Data Security Hubei Key Laboratory of Distributed System Security School of Cyber Science and Engineering, Huazhong University of Science and Technology
• Jamal Bentahar Concordia University
• Rachida Dssouli

Keywords

• Commitment Protocol
• Symbolic Model Checking