IARCS Verification Seminar Series



Title: Bidding Games on Graphs - In theory and in practice.

Speaker: Suman Sadhukhan    (bio) (bio)


Suman Sadhukhan is currently a postdoctoral researcher at the University of Haifa, primarily working with Guy Avni on Bidding Games on Graphs. He obtained his PhD in 2022 from Inria Rennes where he was advised by Nathalie Bertrand, Nicolas Markey and Ocan Sankur, and worked on dynamic network congestion games from a verification perspective. He is interested in, but not restricted to, Games on Graphs, studying different game theoretic models from formal verification and reactive synthesis viewpoint. Prior to his PhD training, he was a student at Chennai Mathematical Institute where he studied Theoretical Computer Science and Mathematics.



When: Tuesday, 19 March 2024 at 1900 hrs (IST)   Slides  Video  

Abstract:
In a two-player zero-sum graph game, the players move a token throughout the game, producing an infinite play, which determines the winner of the game. Bidding games are graph games in which in each turn, a bidding (auction) determines which player moves the token: the players have budgets, and in each turn, both players simultaneously submit the bids that do not exceed the available budgets. The higher bidder moves the token, and pays the bid to the lower bidder (called Richman bidding). The standard solution concept of interest in bidding games are threshold budgets: the necessary and sufficient budget for winning the game.

In this survey talk, on the theoretical side, we will explore discrete bidding games, where the keyword discrete stands for the bids having a fixed granularity. We obtain membership in NP ∩ coNP for solving parity bidding games with exponentially succinct representation. This will be followed by our newly proposed application of bidding games to a decentralized synthesis problem for multi-objective decision making. Here, synthesized policies express their scheduling urgency via bids and a bounded budget guarantees long-run fairness. Moreover, our proposed solution framework is modular, in the sense that if one objective changes, we may still combine the policy for the other objective without having the need to recompute it from scratch.

These works have been in collaboration with Guy Avni and Kaushik Mallik.