Automated Analysis of Commitment Protocols Using Probabilistic Model Checking

8 years 1 months ago

Download www.ntu.edu.sg

Commitment protocols provide an effective formalism for the regulation of agent interaction. Although existing work mainly focus on the design-time development of static commitment protocols, recent studies propose methods to create them dynamically at run-time with respect to the goals of the agents. These methods require agents to verify new commitment protocols taking their goals, and beliefs about the other agents’ behavior into account. Accordingly, in this paper, we ﬁrst propose a probabilistic model to formally capture commitment protocols according to agents’ beliefs. Secondly, we identify a set of important properties for the veriﬁcation of a new commitment protocol from an agent’s perspective and formalize these properties in our model. Thirdly, we develop probabilistic model checking algorithms with advanced reduction for efﬁcient veriﬁcation of these properties. Finally, we implement these algorithms as a tool and evaluate the proposed properties over differe...

Akin Günay, Songzheng Song, Yang Liu, Jie Zha

Real-time Traffic