Accepted author manuscript, 578 KB, PDF document
Available under license: CC BY-NC: Creative Commons Attribution-NonCommercial 4.0 International License
Final published version
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
TY - GEN
T1 - Compositional Correctness for Multiagent Interactions
AU - V, Samuel H. Christie
AU - Chopra, Amit K.
AU - Singh, Munindar P.
N1 - Conference code: 17
PY - 2018/7/10
Y1 - 2018/7/10
N2 - 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.
AB - 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.
M3 - Conference contribution/Paper
SN - 9781450356497
SP - 1159
EP - 1167
BT - Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems
A2 - Dastani, M.
A2 - Sukthankar, G.
A2 - Andre, E.
A2 - Koenig, S.
PB - IFAAMAS
CY - Richmond SC
T2 - 17th International Conference on Autonomous Agents and Multi-agent Systems
Y2 - 10 July 2018 through 15 July 2018
ER -