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

Electronic data

  • Atomicity-shc-v94

    Accepted author manuscript, 577 KB, PDF document

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

Links

View graph of relations

Compositional Correctness for Multiagent Interactions

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

Published
Close
Publication date10/07/2018
Host publicationProceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems
EditorsM. Dastani, G. Sukthankar, E. Andre, S. Koenig
Place of PublicationRichmond SC
PublisherIFAAMAS
Pages1159-1167
Number of pages9
ISBN (Print)9781450356497
Original languageEnglish
Event17th International Conference on Autonomous Agents and Multi-agent Systems - Stockholm, Sweden
Duration: 10/07/201815/07/2018
Conference number: 17

Conference

Conference17th International Conference on Autonomous Agents and Multi-agent Systems
Abbreviated titleAAMAS 2018
CountrySweden
CityStockholm
Period10/07/1815/07/18

Conference

Conference17th International Conference on Autonomous Agents and Multi-agent Systems
Abbreviated titleAAMAS 2018
CountrySweden
CityStockholm
Period10/07/1815/07/18

Abstract

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.