Game Forms for Coalition Effectivity Functions

Baston, Colm; Capretta, Venanzio

Abstract

Introduction Coalition logic, introduced by Pauly, 1 is a multi-agent modal logic for reasoning about what groups of agents can achieve if they act collectively, as a coalition. The semantics for coalition logic is based on game forms, which are essentially perfect-information strategic games where the players act simultaneously. From a game form, we can derive an effectivity function which defines which subsets of outcomes a particular coalition of players can guarantee, regardless of how all other players act. Pauly proves that there is a set of properties, playability, that precisely describe when an arbitrary effectivity function is the effectivity function for some strategic game. Our goal is to formalise this equivalence in the logic of a type-theoretic proof assistant, specifically Coq and Agda. Proving the playability of an effectivity function that is derived from a game form is straightforward, provided that we develop good libraries for decidable subsets of agents and states. The other direction is more complex, requiring the construction of a game form from a playable effectivity function, then proving that the derived effectivity function is equivalent to the function that we started with. We believe that Pauly's proof of the second direction can be simplified in addition to adapting it for type-theoretic formalisation, and we give a sketch of this below.

Citation

Baston, C., & Capretta, V. (2019). Game Forms for Coalition Effectivity Functions. In N. van der Weide, & M. Bezem (Eds.), 25th International Conference onTypes for Proofs and Programs (TYPES 2019), 26-27

• Conference Name: 25th International Conference onTypes for Proofs and Programs (TYPES 2019)
• Start Date: Jun 11, 2019
• End Date: Jun 14, 2019
• Acceptance Date: Apr 15, 2019
• Online Publication Date: Jun 11, 2019
• Publication Date: Jun 11, 2019
• Deposit Date: Sep 27, 2019
• Publicly Available Date: Oct 21, 2019
• Pages: 26-27
• Book Title: 25th International Conference onTypes for Proofs and Programs (TYPES 2019)
• Public URL: https://nottingham-repository.worktribe.com/output/2681068
• Related Public URLs: https://cas.oslo.no/types2019/