Infinite-Duration Richman Bidding Games

Authors: Guy Avni, Thomas A. Henzinger and Ventsislav Chonev

Paper Information

Title:Infinite-Duration Richman Bidding Games
Authors:Guy Avni, Thomas A. Henzinger and Ventsislav Chonev
Proceedings:SR SR18 papers
Editors: Nicolas Markey and Patricia Bouyer
Keywords:Bidding games, Richman games, Parity games, Mean-payoff 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 is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the {\em bidding} mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate {\em budgets}, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. Reachability bidding games, called {\em Richman games}, have been studied in \cite{LLPU96,LLPSU99}. There, a central question is the existence and computation of {\em threshold} budgets; namely, a value $t \in [0,1]$ such that if \PO's budget exceeds $t$, he can win the game, and if \PT's budget exceeds $1-t$, he can win the game. We focus on parity and mean-payoff games. We show the existence of threshold budgets and show that the complexity of finding them coincides with the $NP \cap coNP$ complexity of reachability bidding games. The solution for mean-payoff consists of our most technically challenging contribution, where we construct optimal strategies for the players while extending and generalizing the probabilistic connection that was known for reachability bidding games.

Talk:Jul 08 14:00 (Session 40Q: Two-player games)