Decidable fragments of First Order Modal Logic�(in the context of Large Anonymous games)

Anantha Padmanabha�IIT Madras��Joint work with R. Ramanujam and Ramit Das��12-02-2025�Recent Trends in Logic and Game Theory

Madras School of Economics

​

Large Games

2

• Games where there are a large number of players
• Voting
• Share Market��
• The number of players is large but finite

Large Anonymous Games

3

• Typically payoff depends on the action chosen by the player
• Two different players might get different payoffs for choosing the same action�
• In Anonymous games, payoff does not depend on the identity of the player
• Everyone who chooses a particular choice wins
• Everyone who chooses a particular online delivery app gets the same payoff�
• Payoff depends on how many people choose a particular action�

Payoffs

4

• Payoff in n player game where each player can choose one of the actions from {u v w} :
• An action profile : (u v u u … w) is mapped to payoff (p1 p2 …. pn)�
• In Large Anonymous games :
• (u v u u… w) ( #u , #v, #w ) ( p1, p2, p3 )��� (p1, p2, p1, p1 ……… p3 )

Goal of the talk

5

• Look at Logics to express properties over large anonymous games
• Specify Strategies
• Specify Player Types
• Specify Game properties�
• Can we have a notion of equivalence between two large games?

Strategy Specification

6

• What kind of strategies would playes use in large games?�
• I will always choose action u
• If half of the players choose action u then I will choose action v

​

• I will choose whatever my friend chooses
• I will play u or v with probability 0.5 and 0.5�
• How to refer to players if we do not have access to player identities?
• Use quantification and player types (There exists a player …. )
• Payoff would be determined via player types

Strategy Specification : Distribution Constraint Formulas

7

• Step 1: Specifying the distribution of players
• #a <= ⅓ Atmost ⅓ rd of the players choose action a
• ¬ (#a <= ⅓ ) At least ⅓ rd of the players choose action a
• (#a <= ⅓) ∨ (#b >= ½) �At most ⅓ rd of players choose a or atleast ½ of the players choose b��
• Syntax of Distribution Constraint Formula :
• δ ::= #a <= r | #a >= r | ¬ δ | δ ∨ δ��r is a rational number, a is an action

Strategy Specification : Distribution Constraint Formulas

8

• Distribution Constraint Formula is evaluated at a given strategy profile

​

Strategy Specification : Distribution Constraint Formulas

9

• Not all Distribution Constraint formulas are feasible
• #a >= ⅔ ∧ #b >= ⅔ (Not Feasible)
• If Actions = { a, b} then #a < ½ ∧ #b < ½ (Not Feasible)
• #a = 3/7 ∧ #b >= ⅖ ∧ #c > 0 �(Feasible in infinitely many distributions)
• Can have many scenarios like (15, 14, 6) or (60, 56, 24) ….�
• Given a Distribution Constraint formula, can we check if it is feasible or not?
• Doable using Gaussian elimination
• Corollary : If a distribution constraint formula is satisfiable then it is satisfiable in some game with at most 2^{n^2} players where n is the length of the distribution constraint formula

Strategy Specification : Player Type Formulas

10

• Step 2: Specifying the player types
• (#b <= ½) → a �If at most half of the players play b then I will play a
• (#b <= ½) → a ∨ (#c >= ⅓ ) → b�If at most ½ of the players play b then I will play a (or) �If at least ⅓ rd of the players play c then I will play b

�

• Syntax of Player Type Formulas :
• 𝛼 = δ → a | 𝛼 ∨ 𝛼′ | 𝛼 ∧ 𝛼′

Strategy Specification : Player Type Formulas

11

• Player Type Formula is evaluated at a given strategy profile for a player i���������
• A player type formula can force at most 2^{n^2} players where n is the length of the player type formula

​

​

Game Specification

12

• Step 3: (MIQ STRAT) Specifying the properties of the game
• p < q�Players prefer payoff p to payoff q �(We assume same preference order for all players)
• ( 𝛼 @ i ) Player i is of type 𝛼
• p@i Player i gets payoff p
• a@i Player i plays action a
• ⟨∃⟩φ There exists a group of players who can enforce a � new profile where φ holds

​

Modelling large games : Improvement Graphs

13

• Every game can be associated with a notion of Improvement Graph to study the Game Dynamics�
• Vertices are all possible strategy profiles
• Edges are labelled :
• A-labelled edge from profile 𝞂 to profile 𝞂’ means �Players in the set A can change their strategy to get better payoff (nobody else changes their action)�
• For a given game, Improvement graph is exponential in the number of players

Properties of games as properties of Improvement graphs

14

• Nash Equilibrium :
• Node without any outgoing edges [∀]丄�
• Every improvement path is finite ♢*[∀]丄�
• Equilibrium is reachable from every strategy profile� ☐*♢*[∀]丄

​

Game Specification

15

• MIQ STRAT formulas are evaluated over Improvement Graphs

Axiomatization

16

Axiomatization

17

Axiomatization

18

Axiomatization

19

• (A7), (A8) and (A9)��
• Some Inference Rules

Satisfiability Problem

20

• Given a formula, does there exist a game in which the formula is true?��
• We can get an algorithm that runs in Non-deterministic Double exponential time
• Uses the property that player types can force at most exponential number of players

​

Game Specification

21

• We also have a Monadic Second Order Variant of Game Specification Logic
• Undecidable�
• But can express more properties

​

Game Equivalence

22

• When can we say two games are “equivalent”
• There is no MIQ STRAT formula that can distinguish between the two games�
• If the improvement graphs of the two games are “bisimilar”
• Bisimilar strategy profiles satisfy the following conditions:
• For every action a, ratio of players playing a should be the same
• Every player playing the same action gets the same payoff
• Back and Forth property�
• Two games are “bisimilar” iff they agree on all MIQ STRAT formulas

​

​

Conclusion

23

• Introduced Logic to reason about strategizing in Large anonymous games�
• Expressive power of the logic needs to be studied�
• Extensions of MIQ STRAT that remains decidable�
• Characterizing majority / minority games
• Special kinds of Large Anonymous Games�
• Coalitions and cooperation games

Thank You

24