A Logical Study of the Improvement Graphs formed from Games [HBNI Th234]

Abstract

This work is about analysing reasoning about games - specially the social network games, polymatrix games, priority separable games and large games. Towards the reasoning we employ di↵erent logics - namely the least fixed point logic and a multi modal logic with the reachability operator. We highlight expressibility of game theoretic properties of interest like - Nash Equilibrium, Finite Improvement Paths, Weak Acyclity. We have results where we initially fix the number of players for the game and also, where we try to have the same hold for an arbitrary set of players. We use the monadic variant of least fixed point logic (MLFP) to express the Nash Equilibrium for separable games like priority separable and polymatrix games. We also show how the framework of Improvement Graphs with the logic of MLFP is interesting enough to be able to similarly express notions in the connected literature of Fair Division and Voting. Our hope is to fully flesh out this framework so that we have transfer results from one domain to the other. We use variants of multi modal logics with added capabilities required to have access to games. We show a complete axiomatisation of the logic for our respective games of threshold reasoning in social network games and large games. We also show bisimulation for the both the modal logics respectively. We also come up with a Monadic Second Order Logic of Strategization for Large Games. The logic turns out to be undecidable that is we have a proof for its finite satisfiability being undecidable.