Design time analysis of multiagent protocols

Interaction protocols enable agents to communicate with each other effectively. Whereas several approaches exist to specify interaction protocols, none of them has design tools that can help protocol designers catch semantic protocol errors at design time. As research in networking protocols has shown, flawed specifications of protocols can have disastrous consequences. Hence, it is crucial to systematically analyze protocols in time to ensure effective specification. This paper first studies and formalizes important generic properties of commitment protocols that can ease their effective and consistent development significantly. Next, we identify robustness properties of protocols that are useful in determining the applicability of protocols in different settings. Since these properties are formal, they can easily be incorporated in a software tool to (semi-)automate the design and specification of commitment protocols. Where appropriate we provide algorithms that can directly be used to check these properties in such a design tool.