Protocol Refinement: Formalization and Verification

A proper definition of protocols and protocol refinement is crucial to designing multiagent systems. Rigidly defined protocols can require significant rework for even minor changes. Loosely defined protocols can require significant reasoning capabilities within each agent. Protocol definitions based on commitments is a middle ground. The authors formalize a model of protocols consisting of agent roles, propositions, and commitments. They define protocol refinement between a super-protocol and a sub-protocol by mapping super-protocol elements to corresponding sub-protocol elements. Mapping protocol commitments depends on a novel operation called serial composition.