Composing and verifying commitment-based multiagent protocols

We consider the design and enactment of multiagent protocols that describe collaboration using "normative" or "social" abstractions, specifically, commitments. A (multiagent) protocol defines the relevant social states and how they progress; each participant maintains a local projection of these states and acts accordingly. Protocols expose two important challenges: (1) how to compose them in a way that respects commitments and (2) how to verify the compliance of the parties with the social states. Individually, these challenges are inadequately studied and together not at all. We motivate the notion of a social context to capture how a protocol may be enacted. A protocol can be verifiably enacted when its participants can determine each other's compliance. We first show the negative result that even when protocols can be verifiably enacted in respective social contexts, their composition cannot be verifiably enacted in the composition of those social contexts. We next show how to expand such a protocol so that it can be verifiably enacted. Our approach involves design rules to specify composite protocols so they would be verifiably enactable. Our approach demonstrates a use of dialectical commitments, which have previously been overlooked in the protocols literature