无限期竞价博弈
Infinite-Duration Bidding Games
摘要：
图上的二人游戏在形式化方法中得到了广泛的研究，因为它们模拟了系统与环境之间的交互。游戏通过在整个图中移动代币来产生无限路径来进行。有几种常见的模式来确定玩家如何在图中移动代币;例如，在基于回合的游戏中，玩家在移动代币时交替回合。我们研究了移动令牌的{ \em出价}模式，据我们所知，这在无限持续时间的游戏中从未被研究过。下面的竞价规则是以前定义的，称为Richman竞价。两个参与者都有单独的{ \em预算}，合计为$1$。在每一轮中，都会发生一次出价：两个玩家同时提交出价，如果出价不超过可用预算，则出价是合法的，出价更高的出价者向另一个玩家支付他的出价并移动代币。竞价博弈中研究的中心问题是赢得博弈的必要且充分的初始预算：顶点中的{ \em阈值}预算是一个值$t \in [0,1]$，使得如果参与者$1$的预算超过$t$，他可以赢得博弈，如果参与者$2$的预算超过$1-t$，他可以赢得博弈。阈值预算以前被证明存在于可达性博弈的每个顶点，这与{ \em random-turn}博弈有一个有趣的联系-一个简单的随机博弈的子类，其中移动的玩家是随机选择的。我们证明了存在的阈值预算的定性类的无限持续时间的游戏，即平价游戏，和定量类，即平均收益游戏。证明的关键组成部分是一个定量的解决方案，强连接的平均支付投标游戏中，我们扩展与随机回合游戏这些游戏的连接，并构建明确的最优策略，为双方球员。
英文摘要：
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. The following bidding rule was previously defined and called Richman bidding. Both players have separate {\em budgets}, which sum up to $1$. In each turn, a bidding takes place: Both players submit bids simultaneously, where a bid is legal if it does not exceed the available budget, and the higher bidder pays his bid to the other player and moves the token. The central question studied in bidding games is a necessary and sufficient initial budget for winning the game: a {\em threshold} budget in a vertex is a value $t \in [0,1]$ such that if Player $1$'s budget exceeds $t$, he can win the game, and if Player $2$'s budget exceeds $1-t$, he can win the game. Threshold budgets were previously shown to exist in every vertex of a reachability game, which have an interesting connection with {\em random-turn} games -- a sub-class of simple stochastic games in which the player who moves is chosen randomly. We show the existence of threshold budgets for a qualitative class of infinite-duration games, namely parity games, and a quantitative class, namely mean-payoff games. The key component of the proof is a quantitative solution to strongly-connected mean-payoff bidding games in which we extend the connection with random-turn games to these games, and construct explicit optimal strategies for both players.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
