摘要:In two-player games on graphs, the players move a token through a graph toproduce an infinite path, which determines the winner of the game. Such gamesare central in formal methods since they model the interaction between anon-terminating system and its environment. In bidding games the players bidfor the right to move the token: in each round, the players simultaneouslysubmit bids, and the higher bidder moves the token and pays the other player.Bidding games are known to have a clean and elegant mathematical structure thatrelies on the ability of the players to submit arbitrarily small bids. Manyapplications, however, require a fixed granularity for the bids, which canrepresent, for example, the monetary value expressed in cents. We study, forthe first time, the combination of discrete-bidding and infinite-durationgames. Our most important result proves that these games form a largedetermined subclass of concurrent games, where determinacy is the strongproperty that there always exists exactly one player who can guarantee winningthe game. In particular, we show that, in contrast to non-discrete biddinggames, the mechanism with which tied bids are resolved plays an important rolein discrete-bidding games. We study several natural tie-breaking mechanisms andshow that, while some do not admit determinacy, most natural mechanisms implydeterminacy for every pair of initial budgets.
关键词:Computer Science - Computer Science and Game Theory; Computer Science - Logic in Computer Science