Home > Research > Publications & Outputs > Compositional Correctness for Multiagent Intera...

Electronic data

  • Atomicity-shc-v94

    Accepted author manuscript, 578 KB, PDF document

    Available under license: CC BY-NC: Creative Commons Attribution-NonCommercial 4.0 International License


View graph of relations

Compositional Correctness for Multiagent Interactions

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review



An interaction protocol specifies the constraints on communication between agents in a multiagent system. Ideally, we would like to be able to treat protocols as modules and compose them in a declarative manner to systematically build more complex protocols. Supporting composition correctly requires taking into account information-based causality relationships between protocols. One important problem that may arise from inadequate consideration of such relationships is that the enactment of a composite protocol may violate atomicity ; that is, some components may be initiated but prevented from completing. We use the well-known all or nothing principle as the basis for formalizing atomicity as a novel correctness property for protocols. Our contributions are the following. One, we motivate and formalize atomicity and highlight its distinctiveness from related correctness notions. Two, we give a decision procedure for verifying atomicity and report results from an implementation. For concreteness of exposition and technical development, we adopt BSPL as an exemplar of information causality approaches.