Working Seminar on Formal Models, Discrete Structures, and Algorithms

Infinite-Duration Bidding Games

Guy Avni (IST Austria)

When: Monday November 27, 2 pm

Where: room C417


Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. Two ways to classify graph games is according to the “objective of the players”, e.g., reachability, Buchi, etc., and according to the mode of moving the token, e.g., in turn-based games the players alternate turns in moving the token, and other modes are probabilistic and concurrent moves.

In the talk I will present a new mode of moving the token called “bidding” in which the players “bid” for the right to move the token. The bidding rules are as follows. Both players have separate budgets, which sum up to 1. In a bidding, the players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The player who bids higher wins the bidding, pays his bid to the other player, and moves the token. “Bidding” is the mode of moving, and can be studied with any objective. Reachability bidding games where introduced in the 90s and we study parity and mean-payoff bidding games. We answer the natural questions that arise in these games: “how much initial budget is needed in order to guarantee winning?” and “assuming a sufficient budget, how does one win the game?”. I will close by describing future directions.

Joint work with Thomas Henzinger, Rasmus Ibsen-Jensen, and Ventsislav Chonev