Bidding Games with Charging

TL;DR

The paper extends bidding games by introducing charging: vertex-dependent rewards that can replenish budgets, yielding richer dynamics and non-unique fixed points. It defines thresholds $Th_i(v)$ as the minimal budgets guaranteeing victory from each vertex and proves determinacy for reachability, Büchi, safety, and co-Büchi objectives, though with more complex fixed-point structures than in traditional bidding games. A novel fixed-point algorithm and a mixed-integer linear programming encoding are developed to compute thresholds, and the paper establishes NP-hardness and coNP-hardness results for Rabin and Streett objectives, respectively. It also studies a repair problem: given a budget for charges, can we distribute charges to ensure a target threshold is met, with PSPACE/2EXPTIME bounds for safety/reachability cases, respectively. The results expand the applicability of bidding games to long-run safety and scheduling scenarios where resource replenishment occurs.

Abstract

Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules, and the winner is decided based on the infinite path traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent charges. Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. We show that the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?

Figures (1)

• Figure 1: Examples to demonstrate the distinctive features of bidding games with charging, compared to traditional bidding games (without charging). The double circled vertices are the ones that Player 1 wants to reach (reachability objective), or, dually, the ones that Player 2 wants to avoid (safety objective). When a vertex $v$ has nonzero reward for at least one of the players, the rewards are shown next to $v$ in the vector notation $R_1(v)R_2(v)$. The threshold budget of Player 1 for each vertex is shown in blue next to the vertex.

Theorems & Definitions (2)

• Example 1
• Example 2