Infinite-Duration Bidding Games

Abstract:

Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game proceeds by placing a token on a vertex and having the players move it through the graph to produce an infinite path, which determines the winner or payoff of the game. 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. Two bidding rules have been studied. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar only that the winner of the bidding pays the "bank" rather than the other player. We study infinite-duration bidding games with standard objectives. A central quantity in these games is the "ratio" between the two players' initial budgets. The questions we study concern a necessary and sufficient ratio with which a player can achieve a goal. For qualitative objectives such as parity, we show that the properties of bidding games are largely similar to the properties of bidding reachability games, which where studied in the 90s. Our most interesting results concern bidding mean-payoff games, where we show constructions of optimal strategies for the players. We also show surprising differences between the bidding rules. Unlike in the Richman case, where the optimal payoff is only determined by the structure of the game, in poorman bidding, with a higher ratio, a player can achieve a better payoff. This is shown via a connection with probabilistic games.

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