Determinacy in Discrete-Bidding Infinite-Duration Games

TL;DR

This paper investigates discrete-bidding infinite-duration games on graphs, establishing their determinacy and analyzing how tie-breaking mechanisms influence the existence of guaranteed winning strategies for players.

Contribution

It introduces the study of discrete-bidding in infinite-duration games and proves that most natural tie-breaking mechanisms ensure game determinacy.

Findings

Discrete-bidding games form a large determined subclass of concurrent games.

Tie-breaking mechanisms significantly affect game determinacy.

Most natural tie-breaking rules guarantee determinacy for all initial budgets.

Abstract

In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit 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 that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets.

Full text

1. Introduction

Two-player infinite-duration games on graphs are a central class of games in formal verification [4] and have deep connections to foundations of logic [38]. They are used to model the interaction between a system and its environment, and the problem of synthesizing a correct system then reduces to finding a winning strategy in a graph game [37]. A graph game proceeds by placing a token on a vertex in the graph, which the players move throughout the graph to produce an infinite path (“play”) $\pi$. The winner of the game is determined according to $\pi$.

Two ways to classify graph games are according to the type of objectives of the players, and according to the mode of moving the token. For example, in reachability games, the objective of Player $1$ is to reach a designated vertex $t$, and the objective of Player $2$ is to avoid $t$. An infinite play $\pi$ is winning for Player $1$ iff it visits $t$. The simplest mode of moving is turn based: the vertices are partitioned between the two players and whenever the token reaches a vertex that is controlled by a player, he decides how to move the token.

In bidding games, in each turn, a bidding takes place to determine which player moves the token. Bidding games were introduced in [27, 28], where the main focus was on a concrete bidding rule, called Richman rule (named after David Richman), which is as follows: Each player has a budget, and before each move, the players simultaneously submit bids, where a bid is legal if it does not exceed the available budget. The player who bids higher wins the bidding, pays the bid to other player, and moves the token.

Bidding games exhibit a clean and elegant theory. The central problem that was previously studied concerned the existence of a necessary and sufficient threshold budget, which allows a player to achieve his objective. Assuming the sum of budgets is $1$, the threshold budget at a vertex $v$, denoted $\texttt{Thresh}(v)$, is such that if Player $1$’s budget exceeds $\texttt{Thresh}(v)$, he can win the game, and if Player $2$’s budget exceeds $1-\texttt{Thresh}(v)$, he can win the game. Threshold budgets are known to exist in bidding reachability games [27, 28] with variants of the first-price bidding rule that is described above. Only reachability Richman-bidding games, however, are equivalent to random-turn games [36], which are a special case of stochastic games [20] in which in each turn, the player who moves is chosen according to a probability distribution. Interestingly, a more general and robust equivalence with random-turn games holds for mean-payoff bidding games, which are infinite-duration games, with Richman bidding [7], poorman bidding [8], which are similar to Richman bidding except that the winner of a bidding pays the “bank” rather than the other player, and taxman bidding [10], which span the spectrum between Richman and poorman bidding.

These theoretical properties of bidding games highly depend on the ability of the players to submit arbitrarily small bids. Indeed, in poorman games, the bids tend to [math] as the game proceeds. Even in Richman reachability games, when the budget of Player $1$ at $v$ is $\texttt{Thresh}(v)+\epsilon$, a winning strategy bids so that the budget always exceeds the threshold budget and, either the game is won or Player $1$’s surplus, namely the difference between his budget and the threshold budget, strictly increases. This strategy uses bids that are exponentially smaller than $\epsilon$.

For practical applications, however, allowing arbitrary granularity of bids is unreasonable. For example, in formal methods, graph games are used to reason about multi-process systems, and bidding naturally models “scrip” systems, which use internal currency in order to prioritize processes. Car-control systems are one example, where different components might send conflicting actions to the engine, e.g., the cruise control component can send the action “accelerate” while the traffic-light recognizer can send “stop”. Bidding then specifies the level of criticality of the actions, yet for this mechanism to be practical, the number of levels of criticality (bids) must stay small. Bidding games can be used in settings in which bids represent the monetary value of choosing an action. Such settings typically have a finite granularity, e.g., cents. One such setting is Blockchain technology [16, 5], where players represent agents that are using the service, and their bids represent transaction fees to the miners. A second such setting is reasoning about ongoing auctions like the ones used in the internet for advertisement allocation [34]. Bidding games can be used to devise bidding strategies in such auctions. Motivation for bidding games also comes from recreational games, e.g., bidding chess [13] or tic-tac-toe111http://biddingttt.herokuapp.com/, where it is unreasonable for a human player to keep track of arbitrarily small and possibly irrational numbers.

In this work, we study discrete-bidding games in which the granularity of the bids is restricted to be natural numbers. A key difference from the continuous-bidding model is that there, the issue of tie breaking was largely ignored, which is possible since one can consider cases where the initial budget does not equal $\texttt{Thresh}(v)$. In discrete-bidding, however, ties are a central part of the game. A discrete-bidding game is characterized explicitly by a tie-breaking mechanism in addition to the standard components, i.e., an arena, the players’ budgets, and an objective. We investigate several tie-breaking mechanisms and show how they affect the properties of the game. Discrete-bidding games with reachability objectives were first studied in [21]. The focus in that paper was on extending the Richman theory to the discrete domain, and we elaborate on their results later in this section.

A central concept in game theory is a winning strategy: a strategy that a player can reveal before the other player, and still win the game. A game is determined if exactly one of the players can guarantee winning the game. The simplest example of a non-determined game is a two-player game called matching pennies: Each player chooses $1$ (“heads”) or [math] (“tails”), and Player $1$ wins iff the parity of the sum of the players’ choices is [math]. Matching pennies is not determined since if Player $1$ reveals his choice first, Player $2$ will choose opposite and win the game, and dually for Player $2$.

Discrete-bidding games are a subclass of concurrent graph games [2], in which in each turn, the players simultaneously select actions, and the joint vector of actions determines the next position. A bidding game ${\mathcal{G}}$ is equivalent to a concurrent game ${\mathcal{G}}^{\prime}$ that is played on the “configuration graph” of ${\mathcal{G}}$: each vertex of ${\mathcal{G}}^{\prime}$ is a tuple $\langle v,B_{1},B_{2},s\rangle$, where $v$ is the vertex in ${\mathcal{G}}$ on which the token is situated, the players’ budgets are $B_{1}$ and $B_{2}$, and $s$ is the state of the tie-breaking mechanism. An action in ${\mathcal{G}}^{\prime}$ corresponds to a bid and a vertex to move to upon winning the bidding. Concurrent games are not in general determined since matching pennies can be modelled as a concurrent game.

The central question we address in this work asks under which conditions bidding games are determined. We show that determinacy in bidding games highly depends on the tie-breaking mechanism under use. We study natural tie-breaking mechanisms, show that some admit determinacy while others do not. The simplest tie-breaking rule we consider alternates between the players: Player $1$ starts with the advantage, when a tie occurs, the player with the advantage wins, and the advantage switches to the other player. We show that discrete-bidding games with alternating tie-breaking are not determined, as we demonstrate below. {exa}

Consider the bidding reachability game that is depicted in Fig. 1. We depict the player who has the advantage with a star. We claim that no player has a winning strategy when the game starts from the configuration $\langle v_{0},1,1^{*}\rangle$, thus the token is placed on $v_{0}$, both budgets equal $1$, and Player $2$ has the tie-breaking advantage. We start by showing that if Player $2$ reveals his first bid before Player $1$, then Player $1$ can guarantee winning the game. There are two cases. First, if Player $2$ bids [math], Player $1$ bids $1$ and draws the game to $t$. Second, if Player $2$ bids $1$, then Player $1$ bids [math], and the game reaches the configuration $\langle v_{1},2,0^{*}\rangle$. Next, both players bid [math] and we reach $\langle v_{2},2^{*},0\rangle$. Player $1$ wins by bidding $1$ twice; indeed, the next two configurations are $\langle v_{0},1^{*},1\rangle$ and either $\langle t,0,2^{*}\rangle$, if Player $2$ bids $1$, or $\langle t,0^{*},2\rangle$, if he bids [math]. The proof that Player $1$ loses when he reveals his first bid before Player $2$ can be found in Theorem 5. ∎

We generalize the alternating tie-breaking mechanism as follows. A transducer is similar to an automaton only that the states are labeled by output letters. In transducer-based tie breaking, a transducer is run in parallel to the game. The transducer reads information regarding the biddings and outputs which player wins in case of a tie. Alternating tie-breaking is a special case of transducer tie-breaking in which the transducer is a two-state transducer, where the alphabet consists of the letters $\top$ (“tie”) and $\bot$ (“no-tie”) and the transducer changes its state only when the first letter is read.

{exa}

We describe another simpler game that is not determined. In a Büchi* game*, Player $1$ wins a play iff it visits an accepting state infinitely often. Consider the Büchi bidding game that is depicted on the left of Fig. 2 with the tie-breaking uses the transducer on the right of the figure. That is, if a tie occurs in the first bidding, Player $2$ wins all ties for the rest of the game, and otherwise Player $1$ wins all ties. Note that for $i\in\{1,2\}$, no matter what the budgets are, if Player $i$ wins all ties, he can win the game. A winning strategy for Player $i$ always bids [math]. Intuitively, the other player must invest a unit of budget for winning a bidding and leaving $v_{i}$, thus the game eventually stays in $v_{i}$. So, the winner of the game is determined according to the outcome of the first bidding. Suppose both players’ initial budgets are positive and Player $2$’s budget is not larger than Player $1$’s, thus Player $2$ cannot force a win in the first bidding. Then, the players essentially play a matching-pennies game in the first round, hence no player has a winning strategy. ∎

We proceed to describe our positive results. For transducer-based tie-breaking, we show that bidding games are determined when the transducer is un-aware of the occurrence of ties. Note that this property of the transducer is also a necessary to ensure determinacy since the transducer in Example 1 is aware of ties. The second tie-breaking mechanism for which we show determinacy is random tie-breaking: a tie is resolved by tossing a coin that determines the winner of the bidding. Finally, a tie-breaking mechanism that was introduced in [21] is advantage based, except that when a tie occurs, the player with the advantage can choose between (1) winning the bidding and passing the advantage to the other player, or (2) allowing the other player to win the bidding and keeping the advantage. Determinacy for reachability games with this tie-breaking mechanism was shown in [21]. The technique that is used there cannot be extended to the other tie-breaking mechanisms we study. We show an alternative proof for advantage-based tie-breaking and extend the determinacy result for richer objectives beyond reachability.

We obtain our positive results by developing a unified proof technique to reason about bidding games, which we call local determinacy. Intuitively, a concurrent game is locally determined if from each vertex, there is a player who can reveal his action before the other player. We show that locally-determined reachability games are determined and then extend to Müller games, which are richer qualitative games. We expect our technique to extend to show determinacy in other fragments of concurrent games unlike the technique in [21], which is tailored for bidding games.

Determinacy has computational complexity implications; namely, finding the winner in a bidding game with objective $\alpha$ when the budgets are given in unary is as hard as solving a turn-based game with objective $\alpha$, and we show a simple reduction in the other way for bidding games. Finally, we establish results for strongly-connected discrete-bidding games.

2. Preliminaries

2.1. Concurrent and turn-based games

A concurrent game is a two-player game that is played by placing a token on a graph. In each turn, both players simultaneously select actions, and the next vertex the token moves to is determined according to their joint actions. The players’ actions give rise to an infinite path $\pi$ in the graph. A game is accompanied by an objective for Player $1$, who wins iff $\pi$ meets his objective. We specify standard objectives in games later in the section. For $i\in\{1,2\}$, we use $-\!i$ to refer to the other player, namely $-\!i=3-i$.

Formally, a concurrent game is played on an arena $\langle A,V,\lambda,\delta\rangle$, where $A$ is a finite non-empty set of actions, $V$ is a finite non-empty set of vertices, the function $\lambda:V\times\{1,2\}\rightarrow 2^{A}\setminus\emptyset$ specifies the allowed actions for Player $i$ in vertex $v$, and $\delta:V\times A\times A\rightarrow V$ specifies, given the current vertex and a choice of actions for the two players, the next vertex the token moves to. We call $u\in V$ a neighbor of $v\in V$ if there is a pair of allowed action $a^{1},a^{2}\in A$ at $v$ with $u=\delta(v,a^{1},a^{2})$. We use $N(v)\subseteq V$ to denote the set of neighbors of $v$. We say that Player $i$ controls a vertex $v\in V$ if his actions uniquely determine where the token proceeds to from $v$. That is, for every $a\in\lambda(v,i)$ there is a vertex $u$ such that, for every allowed action $a^{\prime}$ of Player $-\!i$, we have $\delta(v,a,a^{\prime})=u$. A turn-based game is a special case of a concurrent game in which each vertex is controlled by one of the players.

2.2. Bidding games

A (discrete) bidding game is a special case of a concurrent game. The game is played on a graph and both players have budgets. In each turn, a bidding takes place to determine which player gets to move the token. Formally, a bidding game is played on an arena $\langle V,E,N,{\mathcal{M}}\rangle$, where $V$ is a set of vertices, $E\subseteq(V\times V)$ is a set of edges, $N\in\mathbb{N}$ represents the total budget, and the tie-breaking mechanism is ${\mathcal{M}}$ on which we elaborate below.

We formalize the semantics of a bidding game ${\mathcal{G}}=\langle V,E,N,{\mathcal{M}}\rangle$ by means of a concurrent game $\langle A,V^{\prime},\lambda,\delta\rangle$. For ease of presentation, in a vertex that is controlled by one player, we list only the neighboring vertices rather than specifying the allowed actions. The set of actions correspond to the possible bids, thus $A=\{0,\ldots,N\}$. The vertices are partitioned between configuration vertices and intermediate vertices. Intuitively, biddings occur in configuration vertices. Intermediate vertices are convenient for “book keeping”; the winner chooses the successor vertex and the state of the tie-breaking mechanism is updated. Formally, a configuration vertex is $c=\langle v,B_{1},B_{2},s\rangle$, where $v\in V$ is the vertex on which the token is placed on in the bidding game ${\mathcal{G}}$, for $i\in\{1,2\}$, the budget of Player $i$ is $B_{i}\in\{0,\dots,N\}$, where $B_{1}+B_{2}=N$, and $s$ is the state of the tie-breaking mechanism as we elaborate below. The set of allowed actions in $c$ is $\{0,\ldots,B_{i}\}$ for Player $i$, which, again, corresponds to the legal bids.

An intermediate vertex is $x=\langle c,b_{1},b_{2}\rangle$, where $c=\langle v,B_{1},B_{2},s\rangle$ is a configuration vertex and $b_{i}\in\{0,\ldots,N\}$, for $i\in\{1,2\}$. The neighbors of a configuration vertex $c$ are of the form $\langle c,b_{1},b_{2}\rangle$, for every pair of allowed actions $b_{1}$ and $b_{2}$ for the two players in $c$. Let $b_{1},b_{2}\in\{0,\ldots,N\}$. Suppose $b_{1}>b_{2}$ and the case of $b_{2}>b_{1}$ is dual. Player $1$ wins the bidding at $c$. Let $B^{\prime}_{1}=B_{1}-b_{1}$ and $B^{\prime}_{2}=B_{2}+b_{2}$, thus Player $1$ pays Player $2$ the winning bid. Player $1$ controls the intermediate vertex $x$. Its neighbors are of the form $\langle v^{\prime},B^{\prime}_{1},B^{\prime}_{2},s^{\prime}\rangle$, where $v^{\prime}$ is a neighbor of $v$ in ${\mathcal{G}}$ and $s^{\prime}$ is the updated tie-breaking mechanism as we elaborate below.

We proceed to the case of ties, i.e., when $b_{1}=b_{2}$, and describe three types of tie-breaking mechanisms.

**Transducer-based: **

A transducer is $T=\langle\Sigma,Q,q_{0},\Delta,\Gamma\rangle$, where $\Sigma$ is a set of letters, $Q$ is a set of states, $q_{0}\in Q$ is an initial state, $\Delta:Q\times\Sigma\rightarrow Q$ is a partial deterministic function, and $\Gamma:Q\rightarrow\{1,2\}$ is a labeling of the states. Intuitively, $T$ is run in parallel to the bidding game and its state is updated according to the outcomes of the biddings. Whenever a tie occurs and $T$ is in state $s\in Q$, the winner of the bidding is $\Gamma(s)$. The information according to which tie-breaking is determined is represented by the alphabet of $T$. In general, the information can include the vertex on which the token is located and the result of the previous bidding, i.e., the winner, whether or not a tie occurred, and the winning bid, thus $\Sigma=V\times\{1,2\}\times\{\bot,\top\}\times\mathbb{N}$.

**Random-based: **

A tie is resolved by choosing the winner uniformly at random.

**Advantage-based: **

Exactly one player holds the advantage. Suppose Player $i$ holds the advantage and a tie occurs. Then Player $i$ chooses who wins the bidding. If he calls the other player the winner, Player $i$ keeps the advantage, and if he calls himself the winner, the advantage switches to the other player.

We describe the updates to the tie-breaking mechanism’s state when using the three mechanisms above. Consider a configuration $c=\langle v,B_{1},B_{2},s\rangle$ and an intermediate vertex $\langle c,b_{1},b_{2}\rangle$. With transducer-based mechanism, the state $s$ is a state in the transducer $T$. If $b_{1}\neq b_{2}$, the player who controls $\langle v,b_{1},b_{2}\rangle$ is determined as in the above. In case $b_{1}=b_{2}$, then Player $\Gamma(s)$ controls the vertex. In both cases, we update the state of the tie-breaking mechanism by feeding it the information on the last bidding; who won, whether a tie occurred, and what vertex the winner chose, thus we set $s^{\prime}=\Delta(s,\sigma)$, where $\sigma=\langle v^{\prime},i,\bot,b_{i}\rangle$ in case Player $i$ wins the bidding with his bid of $b_{i}$, moves to $v^{\prime}$, and no tie occurs. The other cases are similar.

In random-based tie-breaking, the mechanism has no state, thus we can completely omit $s$. Consider an intermediate vertex $\langle c,b_{1},b_{2}\rangle$. The case of $b_{1}\neq b_{2}$ is as in the above. Suppose both players bid $b$. For ease of presentation we assume $b>0$, and the case of $b=0$ is defined in a similar manner. The intermediate vertex $\langle c,b,b\rangle$ is controlled by “Nature”. It has two probabilistic outgoing transitions; one transition leads to the intermediate vertex $\langle c,b,b-1\rangle$, which represents Player $1$ winning the bidding with a bid of $b$, and the other to the intermediate vertex $\langle c,b-1,b\rangle$, which represents Player $2$ winning the bidding with a bid of $b$. We elaborate on the semantics of concurrent games with probabilistic edges in Section 5.

Finally, in advantage-based tie-breaking, the state of the mechanism represents which player has the advantage, thus $s\in\{1,2\}$. Consider an intermediate vertex $\langle c,b_{1},b_{2}\rangle$. When a tie does not occur, there is no need to update $s$. When $b_{1}=b_{2}$, then Player $s$ controls $\langle c,b_{1},b_{2}\rangle$ and the possibility to choose who wins the bidding. Choosing to lose the bidding is modelled by no update to $s$ and moving to an intermediate vertex that is controlled by Player $-s$ from which he chooses a successor vertex and the budgets are updated accordingly. When Player $s$ chooses to win the bidding we proceed directly to the next configuration vertex, update the budgets, and the mechanism’s state to $3-s$.

2.3. Strategies, plays, and objectives

A strategy is, intuitively, a recipe that dictates the actions that a player chooses in a game. Formally, a finite history of a concurrent game is a sequence $\langle v_{0},a^{1}_{0},a^{2}_{0}\rangle,\ldots,\langle v_{n-1},a^{1}_{n-1},a^{2}_{n-1}\rangle,v_{n}\in(V\times A\times A)^{*}\cdot V$ such that, for each $0\leq i<n$, we have $v_{i+1}=\delta(v_{i},a^{1}_{i},a^{2}_{i})$. A strategy is a function from $(V\times A\times A)^{*}\cdot V$ to $A$. We restrict attention to legal strategies that assign only allowed actions, thus for every history $\pi\in(V\times A\times A)^{*}\cdot V$ that ends in $v\in V$, a legal strategy $\sigma_{i}$ for Player $i$ has $\sigma_{i}(\pi)\in\lambda(v,i)$. Two strategies $\sigma_{1}$ and $\sigma_{2}$ for the two players and an initial vertex $v_{0}$, determine a unique play, denoted $\text{play}(v_{0},\sigma_{1},\sigma_{2})\in(V\times A\times A)^{\omega}$, which is defined as follows. The first element of $\text{play}(v_{0},\sigma_{1},\sigma_{2})$ is $\langle v_{0},\sigma_{1}(v_{0}),\sigma_{2}(v_{0})\rangle$. For $i\geq 1$, let $\pi^{i}$ denote the prefix of length $i$ of $\text{play}(v_{0},\sigma_{1},\sigma_{2})$ and suppose its last element is $\langle v_{i},a^{1}_{i},a^{2}_{i}\rangle$. We define $v_{i+1}=\delta(v_{i},a^{i}_{1},a^{i}_{2})$, $a^{i+1}_{1}=\sigma_{1}(\pi^{i}\cdot v_{i+1})$, and $a^{i+1}_{2}=\sigma_{2}(\pi^{i}\cdot v_{i+1})$. The path that corresponds to $\text{play}(v_{0},\sigma_{1},\sigma_{2})$ is $v_{0},v_{1},\ldots$.

An objective for Player $1$ is a subset of infinite paths $\alpha\subseteq V^{\omega}$. We say that Player $1$ wins $\text{play}(v_{0},\sigma_{1},\sigma_{2})$ iff the path $\pi$ that corresponds to $\text{play}(v_{0},\sigma_{1},\sigma_{2})$ satisfies the objective, i.e., $\pi\in\alpha$. Let $inf(\pi)\subseteq V$ be the subset of vertices that $\pi$ visits infinitely often. We consider the following objectives.

**Reachability: **

A game is equipped with a target set $T\subseteq V$. A play $\pi$ is winning for Player $1$, the reachability player, iff it visits $T$.

Büchi**: **

A game is equipped with a set $T\subseteq V$ of accepting vertices. A play $\pi$ is winning for Player $1$ iff it visits $T$ infinitely often.

**Parity: **

A game is equipped with a function $p:V\rightarrow\{1,\ldots,d\}$, for $d\in\mathbb{N}$. A play $\pi$ is winning for Player $1$ iff $\max_{v\in inf(\pi)}p(v)$ is odd.

Müller**: **

A game is equipped with a set $T\subseteq 2^{V}$. A play $\pi$ is winning for Player $1$ iff $inf(\pi)\in T$.

3. A Framework for Proving Determinacy

3.1. Determinacy

Determinacy is a strong property of games, which intuitively says that exactly one player has a winning strategy. That is, the winner can reveal his strategy before the other player, and the loser, knowing how the winner plays, still loses.

{defi}

[Determinacy] A strategy $\sigma_{i}$ is a winning strategy for Player $i$ at vertex $v$ iff for every strategy $\sigma_{-\!i}$ for Player $-\!i$, Player $i$ wins $\text{play}(v,\sigma_{1},\sigma_{2})$. We say that a game $\langle V,E,\alpha\rangle$ is determined if from every vertex $v\in V$ either Player $1$ has a winning strategy from $v$ or Player $2$ has a winning strategy from $v$.

While concurrent games are not determined (e.g., “matching pennies”), turn-based games are largely determined. {thmC}[[30]] Turn-based games with objectives that are Borel sets are determined. In particular, turn-based Müller games are determined.

We describe an alternative definition for determinacy in concurrent games. Consider a concurrent game ${\mathcal{G}}=\langle A,V,\lambda,\delta,\alpha\rangle$. Recall that in ${\mathcal{G}}$, in each turn, the players simultaneously select an action, and their joint actions determine where the token moves to. For $i\in\{1,2\}$, let ${\mathcal{G}}_{i}$ be the turn-based game that, assuming the token is placed on a vertex $v$, Player $i$ selects an action first, then Player $-\!i$ selects an action, and the token proceeds from $v$ as in ${\mathcal{G}}$ given the two actions. Formally, the game ${\mathcal{G}}_{1}$ is a turn-based game $\langle A,V\cup(V\times A),\lambda^{\prime},\delta^{\prime},\alpha^{\prime}\rangle$, and the definition for ${\mathcal{G}}_{2}$ is dual. The vertices that are controlled by Player $1$ are $V_{1}=V$ and $V_{2}=V\times A$. For $v\in V$, we have $\lambda^{\prime}(v,1)=\lambda(v,1)$ and since Player $1$ controls $v$, we arbitrarily fix $\lambda^{\prime}(v,2)=A$. For $a_{1}\in\lambda(v,1)$ and $a_{2}\in A$, we define $\delta(v,a_{1},a_{2})=\langle v,a_{1}\rangle$. Similarly, we define $\lambda^{\prime}(\langle v,a_{1}\rangle,1)=A$ and $\lambda^{\prime}(\langle v,a_{1}\rangle,2)=\lambda(v,2)$. For $a_{1}^{\prime}\in A$ and $a_{2}\in\lambda(v,2)$, we define $\delta^{\prime}(\langle v,a_{1}\rangle,a_{1}^{\prime},a_{2})=\delta(v,a_{1},a_{2})$. Finally, an infinite play $v_{1},\langle v_{1},a_{1}\rangle,v_{2},\langle v_{2},a_{2}\rangle,\ldots,$ is in $\alpha^{\prime}$ iff $v_{1},v_{2},\ldots$ is in $\alpha$. Recall that in bidding games, intermediate vertices are controlled by one player and the only concurrent moves occur when revealing bids. Thus, when ${\mathcal{G}}$ is a bidding game, in ${\mathcal{G}}_{i}$, Player $i$ always reveals his bids before Player $-\!i$.

Proposition 1**.**

A strategy $\sigma_{i}$ is winning for Player $i$ in ${\mathcal{G}}$ at vertex $v$ iff it is winning in ${\mathcal{G}}_{i}$ from $v$. Then, ${\mathcal{G}}$ is determined at $v$ iff either Player $1$ wins in ${\mathcal{G}}_{1}$ from $v$ or Player $2$ wins in ${\mathcal{G}}_{2}$ from $v$.

3.2. Local and global determinacy

We define local determinacy in a fragment of concurrent games, which slightly generalizes bidding games. We describe the intuition of the definition. Taking a step back, a bidding game has two components: the graph on which the game is played and the budget and tie-breaking mechanism. In a configuration vertex $c=\langle v,B_{1},B_{2},s\rangle$ in a bidding game, the triple $\langle B_{1},B_{2},s\rangle$ determines the available actions for the two players at $c$. The objective is given by the first element of the configuration vertices; namely, a play gives rise to a path in $V^{\omega}$ that determines the winner of the game. In R-concurrent games, we abstract away both elements. Instead of considering the bidding mode of moving, we assume a transducer, denoted $R$, determines the available actions in a configuration vertex. As in bidding games, we allow intermediate vertices between configuration vertices for book-keeping of the state of the transducer. As in bidding games, the objective is determined only by the sequence of configuration vertices that are traversed by a play.

Formally, consider a transducer $R=\langle A\times A,Q,q_{0},\Delta,\Gamma\rangle$, where $\Delta:Q\times A\times A\rightarrow Q$ is a partial function. Let $\lambda:Q\times\{1,2\}\rightarrow 2^{A}\setminus\{\emptyset\}$ be a function that specifies a set of allowed actions for each player at every state. For each $a_{1}\in\lambda(q,1)$ and $a_{2}\in\lambda(q,2)$ we require that $\Delta(q,a_{1},a_{2})$ is defined. Recall that $\Gamma:Q\rightarrow\{1,2\}$. In a transducer that corresponds to a bidding game, each state has the form $\langle B_{1},B_{2},s\rangle$, thus it represents the state of the budgets and the state of the tie-breaking mechanism. The allowed actions for Player $i$ in such a state correspond to the possible bids; namely, for $i\in\{1,2\}$, we have $\lambda(\langle B_{1},B_{2},s\rangle,i)=\{0,\ldots,B_{i}\}$.

We say that a concurrent game ${\mathcal{G}}=\langle A,V,\lambda,\delta,\alpha\rangle$ is $R$-concurrent for a transducer $R$ if (1) the set of vertices $V$ are partitioned into configuration vertices $C$ and intermediate vertices $I$, (2) intermediate vertices do not contribute to the objective, thus for two plays $\pi$ and $\pi^{\prime}$ that differ only in their intermediate vertices, we have $\pi\in\alpha$ iff $\pi^{\prime}\in\alpha$, (3) the neighbors of configuration vertices are intermediate vertices and the transition function restricted to configuration vertices is one-to-one, i.e., for every configuration vertex $c$ and two pairs of actions $\langle a_{1},a_{2}\rangle\neq\langle a^{\prime}_{1},a^{\prime}_{2}\rangle$, we have $\delta(c,a_{1},a_{2})\neq\delta(c,a^{\prime}_{1},a^{\prime}_{2})$, (4) each intermediate vertex is controlled by one player and its neighbors can either be all intermediate or all configuration vertices, (5) for $v,v^{\prime}\in V$ with $v\neq v^{\prime}$ such that $N(v),N(v^{\prime})\subseteq I$, we have $N(v)\cap N(v^{\prime})=\emptyset$, (6) each vertex in $V$ is associated with a state in $R$ with the following restrictions. Suppose $c\in C$ is associated with $q\in Q$. Then, $\lambda(v,i)=\lambda(q,i)$, for $i\in\{1,2\}$. The transducer updates its state after concurrent moves in configuration vertices; namely, for a configuration vertex $c$ and two actions $a_{1},a_{2}\in A$, let $u=\delta(c,a_{1},a_{2})$ be an intermediate vertex. Then, the state that is associated with $u$ is $q^{\prime}=\Delta(q,a_{1},a_{2})$ and $u$ is controlled by Player $\Gamma(q^{\prime})$. The transducer also updates its state between intermediate states; namely, if $u^{\prime}\in I$ is a neighbor of $u$ and assume Player $1$ controls $u$ and chooses action $a_{1}$ to proceed from $u$ to $u^{\prime}$, then $u^{\prime}$ is associated with $\Delta(q^{\prime},a_{1},a_{2})$, for all $a_{2}\in A$, and similarly for Player $2$. Finally, the transducer does not update its state when proceeding from an intermediate vertex to a configuration one; namely, if $c^{\prime}\in C$ is a neighbor of $u\in I$ and $u$ is associated with $q\in Q$, then $c^{\prime}$ is associated with $q$.

Bidding games with transducer- and advantage-based tie-breaking are $R$-concurrent. As in the above, for $N\in\mathbb{N}$, the states of the transducer $R$ are of the form $\langle B_{1},B_{2},s\rangle$, where $B_{1}+B_{2}=N$ and $s$ is the state of the tie-breaking mechanism. Following a bidding in a configuration vertex, the intermediate vertex is obtained as follows. The budgets are updated by reducing the winning bid from the winner’s budget and adding it to the loser’s budget, and the state of the tie-breaking mechanism is updated. With transducer-based tie-breaking, we need only one intermediate vertex between two configuration vertices since we use the information from the bidding to update the state of the tie-breaking transducer. In advantage-based tie-breaking, when no tie occurs, a single intermediate vertex is needed since there is no update to the state of the tie-breaking mechanism. In case of a tie, however, a second intermediate vertex is needed in order to allow the player who holds the advantage, the chance to decide whether or not to use it.

We describe the intuition for local determinacy. Consider a concurrent game ${\mathcal{G}}$ and a vertex $v$. Recall that it is generally not the case that ${\mathcal{G}}$ is determined. That is, it is possible that neither Player $1$ nor Player $2$ have a winning strategy from $v$. Suppose Player $1$ has no winning strategy. We say that a transducer admits local determinacy if in every vertex $v$ that is not winning for Player $1$, there is a Player $2$ action that he can reveal before Player $1$ and stay in a non-losing vertex. Formally, we have the following.

{defi}

[Local determinacy]

We say that a transducer $R$ admits local determinacy if every concurrent game ${\mathcal{G}}$ with Borel objective that is $R$-concurrent has the following property. Consider the turn-based game ${\mathcal{G}}_{1}$ in which Player $1$ reveals his action first in each position. Since $\alpha$ is Borel, it is a determined game and there is a partition of the vertices to losing and winning vertices for Player $1$. Then, for every vertex $v\in V$ that is losing for Player $1$ in ${\mathcal{G}}_{1}$, there is a Player $2$ action $a_{2}$ such that, for every Player $1$ action $a_{1}$, the vertex $\delta(v,a_{1},a_{2})$ is losing for Player $1$ in ${\mathcal{G}}_{1}$.

We show that locally-determined games are determined by starting with reachability objectives and working our way up to Müller objectives.

Lemma 2**.**

If a reachability game ${\mathcal{G}}$ is $R$-concurrent for a locally-determined transducer $R$, then ${\mathcal{G}}$ is determined.

Proof 3.1**.**

Consider a concurrent reachability game ${\mathcal{G}}=\langle A,V,\lambda,\delta,\alpha\rangle$ and a vertex $v\in V$ from which Player $1$ does not have a winning strategy. That is, $v$ is losing for Player $1$ in ${\mathcal{G}}_{1}$. We describe a winning strategy for Player $2$ from $v$ in ${\mathcal{G}}$. Player $2$’s strategy maintains the invariant that the set of vertices $S$ that are visited along the play in ${\mathcal{G}}$, are losing for Player $1$ in ${\mathcal{G}}_{1}$. Recall that since we assume intermediate vertices do not contribute to the objective, the target of Player $1$ is a configuration vertex. The invariant implies that Player $2$ wins since there is no intersection between $S$ and Player $1$’s target, and thus the target is never reached. Initially, the invariant holds by the assumption that $v$ is losing for Player $1$ in ${\mathcal{G}}_{1}$. Suppose the token is placed on a vertex $u$ in ${\mathcal{G}}$. Local determinacy implies that Player $2$ can choose an action $a_{2}$ that guarantees that no matter how Player $1$ chooses, the game reaches a losing vertex for Player $1$ in ${\mathcal{G}}_{1}$. Thus, the invariant is maintained, and we are done.

Next, we show determinacy in parity games by reducing them to reachability games.

Lemma 3**.**

If a parity game ${\mathcal{P}}$ is $R$-concurrent for a locally-determined transducer $R$, then ${\mathcal{P}}$ is determined.

Proof 3.2**.**

Consider a parity game ${\mathcal{P}}=\langle A,V,\delta,\lambda,p\rangle$ that is $R$-concurrent, where $R$ is locally determined. Consider a vertex $v\in V$ from which Player $1$ does not win, and we prove that Player $2$ wins from $v$ in ${\mathcal{P}}$ (see a depiction of the proof in Figure 3). By Proposition 1, for $i\in\{1,2\}$, Player $i$ wins from $v$ in ${\mathcal{P}}$ iff he wins from $v$ in ${\mathcal{P}}_{i}$ in which he reveals his action first.

We use a well-known reduction from parity games to reachability games (see for example, [3]). The cycle-forming game that is associated with ${\mathcal{P}}_{i}$ and $v$, denoted $CFG({\mathcal{P}}_{i},v)$, is a reachability game in which we intuitively play from $v$ in ${\mathcal{P}}_{i}$ until a cycle is formed. The resulting play is a lasso $\pi_{1}\pi_{2}$ and Player $i$ wins iff his objective is met in the infinite play $\pi_{1}\pi_{2}^{\omega}$. Memoryless determinacy of turn-based parity games [22] implies that Player $i$ wins from $v$ in ${\mathcal{P}}_{i}$ iff he wins from $v$ in $CFG({\mathcal{P}}_{i},v)$.

Formally, a vertex in $CFG({\mathcal{P}}_{i},v)$ records the history of the game in ${\mathcal{P}}_{i}$. Recall that in a configuration vertex $c\in V$, Player $i$ reveals his action first, and, assuming he chooses $a\in A$, the following vertex is $\langle c,a\rangle$, and its successors are intermediate vertices. Since intermediate vertices are controlled by one of the players and no concurrent moves take place in these vertices, there is no need to add further intermediate vertices. Note that a cycle can only be closed in configuration vertices. Indeed, recall that for $v,v^{\prime}\in V$, if $N(v),N(v^{\prime})\subseteq I$, then $N(v)\cap N(v^{\prime})=\emptyset$. A vertex of $CFG({\mathcal{P}}_{i},v)$ is a sequence in $(C\times(C\times A)\times I^{*})^{*}$ with no repetitions. Consider a vertex $u=c_{1},(c_{1},a_{1}),d^{1}_{1},\ldots,d^{1}_{n_{1}},c_{2},\ldots,v_{k}$, where $v_{k}$ is in $C\cup(C\times A)\cup I$. If there is an earlier configuration vertex $c_{j}$ with $v_{k}=c_{j}$, then $u$ is a leaf and the winner in it is the winner of the infinite loop as in the above. Otherwise, the player who controls $v_{k}$ in ${\mathcal{P}}_{i}$ controls $u$ and its neighbors are $u\cdot v^{\prime}$, where $v^{\prime}$ is a neighbor of $v_{k}$ in ${\mathcal{P}}_{i}$.

We apply the same cycle-forming game reduction to the original game ${\mathcal{P}}$ starting from the vertex $v$. Vertices in $CFG({\mathcal{P}},v)$ are now of the form $(C\times I^{*})^{*}$. Consider a vertex $u=c_{1},d^{1}_{1},\ldots,d^{1}_{n_{1}},c_{2},\ldots,v_{k}$. We claim that the resulting game is a reachability game that is $R$-concurrent. Indeed, the vertex $u$ is a configuration vertex in $CFG({\mathcal{P}},v)$ iff $v_{k}$ is a configuration vertex, and the state in $R$ that $u$ is associated with is the same as $v_{k}$. If $v_{k}$ is a configuration vertex, then the allowed actions of the two players in $u$ are the same as in $v_{k}$. The rest of the construction follows the same lines as the one above. By Lemma 2, the game $CFG({\mathcal{P}},v)$ is determined, thus if Player $1$ does not win from $v$ in $CFG({\mathcal{P}},v)$, then Player $2$ wins from $v$ in $CFG({\mathcal{P}},v)$.

For $i\in\{1,2\}$, we construct $CFG({\mathcal{P}},v)_{i}$ by requiring Player $i$ to reveal his choice before Player $-\!i$ in configuration vertices. Note that $CFG({\mathcal{P}}_{i},v)$ and $CFG({\mathcal{P}},v)_{i}$ have a slight technical difference; namely, vertices in $CFG({\mathcal{P}},v)_{i}$ lack the intermediate vertices in $C\times A$. Since the transition function in ${\mathcal{P}}$ is one-to-one when restricted to configuration vertices, the vertex between $c_{j}$ and $d^{j}_{i}$ can be uniquely deduced. Thus, Player $i$ wins from $v$ in $CFG({\mathcal{P}}_{i},v)$ iff Player $i$ wins from $v$ in $CFG({\mathcal{P}},v)_{i}$.

We combine the reductions: If Player $1$ does not win from $v$ in ${\mathcal{P}}$, by definition, he loses from $v$ in ${\mathcal{P}}_{1}$, thus due to memoryless determinacy in turn-based games, he also loses from $v$ in $CFG({\mathcal{P}}_{1},v)$ and, due to the equivalence between the games, also in $CFG({\mathcal{P}},v)_{1}$. Determinacy for reachability games implies that Player $2$ wins from $v$ in $CFG({\mathcal{P}},v)_{2}$, and going in the other direction, we obtain that Player $2$ wins from $v$ in ${\mathcal{P}}$, and we are done.

The proof for Müller objectives is similar only that we replace the cycle-forming game reduction with a reduction from Müller games to parity games [25, Chapter $2$].

Theorem 4**.**

If a Müller game ${\mathcal{G}}$ is $R$-concurrent for a locally-determined transducer $R$, then ${\mathcal{G}}$ is determined.

3.3. The bidding matrix

Consider a bidding game ${\mathcal{G}}=\langle V,E,N,{\mathcal{M}},\alpha\rangle$. Recall that ${\mathcal{G}}$ is $R$-concurrent, where a configuration vertex is of the form $c=\langle v,B_{1},B_{2},s\rangle$. The set of allowed actions in $c$ for Player $i$ is $\{0,\ldots,B_{i}\}$, for $i\in\{1,2\}$. In particular, there is a natural order on the actions. We think of the possible pairs of actions available in $c$ as a matrix $M_{c}$, which we call the bidding matrix. Rows in $M_{c}$ correspond to Player $1$ bids and columns corresponds to Player $2$ bids. The diagonal that starts in the top-left corner of $M_{c}$ and follows entries of the form $\langle j,j\rangle$, for $0\leq j\leq\min\{B_{1},B_{2}\}$, corresponds to biddings that resolve in a tie. Entries above and below it correspond to biddings that are winning for Player $2$ and Player $1$, respectively. Consider the turn-based game ${\mathcal{G}}_{1}$ in which Player $1$ reveals his bid first. We consider objectives for which turn-based games are determined, thus in ${\mathcal{G}}_{1}$, the vertex $\langle c,b_{1},b_{2}\rangle$ is either winning for Player $1$ or Player $2$. The entries in $M_{c}$ are in $\{1,2\}$, where $M_{c}(b_{1},b_{2})=1$ iff the intermediate vertex $\langle c,b_{1},b_{2}\rangle$ is winning for Player $1$ in ${\mathcal{G}}_{1}$.

For $i\in\{1,2\}$, we call a row or column in $M_{c}$ an $i$-row or $i$-column, respectively, if all its entries are $i$. We rephrase local determinacy in bidding games in terms of the bidding matrix.

{defi}

Consider a bidding game ${\mathcal{G}}=\langle V,E,N,{\mathcal{M}},\alpha\rangle$. We say that ${\mathcal{G}}$ is locally determined if for every configuration vertex $c$, the bidding matrix either has a $2$-column or a $1$-row.

It is not hard to show that Definition 3.3 implies Definition 3.2. Consider a bidding game ${\mathcal{G}}$ in which in each configuration vertex $c$ there is either a $1$-row or a $2$-column in $M_{c}$. We claim that ${\mathcal{G}}$ is locally determined. Suppose $c$ is losing for Player $1$ in ${\mathcal{G}}_{1}$, we need to show that there is a Player $2$ action (bid) that he can reveal before Player $1$ and that guarantees that the game stays in a losing vertex for Player $1$. In other words, we need to show that a $2$-column exists. We rule out the possibility of a $1$-row in $M_{c}$. This is immediate since if there was a $1$-row, Player $1$ could use the corresponding bid, direct the game to a vertex from which he wins, and use the winning strategy from there, contradicting the fact that $c$ is losing for Player $1$.

4. Transducer-based tie-breaking

The determinacy of bidding games with transducer-based tie-breaking depends on the information that is available to the transducer. We start with a negative result.

Theorem 5**.**

Reachability bidding games with alternate tie-breaking are not determined.

Proof 4.1**.**

Consider the bidding reachability game that is depicted in Fig. 1. We show that no player has a winning strategy when the game starts from the configuration $\langle v_{0},1,1^{*}\rangle$, thus the token is placed on $v_{0}$, both budgets equal $1$, and Player $2$ has the tie-breaking advantage. The proof that Player $2$ has no winning strategy is shown in Example 1. We show that Player $1$ has no winning strategy, thus if he reveals his first bid before Player $2$, then Player $2$ wins the game. In Fig. 4, we depict most of the relevant configurations in the game with Player $2$’s strategy in place. Consider the configuration $\langle v_{0},1,1^{*}\rangle$, and we assume Player $2$ reveals his bid after Player $1$. For example, if Player $1$ bids [math], Player $2$ bids [math], wins the bidding since he holds the advantage, and the game proceeds to the configuration $\langle v_{1},1^{*},1\rangle$. Similarly, if Player $1$ bids $1$, Player $2$ bids $1$, and the game proceeds to $\langle v_{1},2^{*},0\rangle$. For readability, we omit from the figure some configurations so some configuration have no outgoing edges. It is not hard to show that Player $2$ can force the game from these configurations back to one of the depicted configurations. Thus, when Player $1$ reveals his bids first, Player $2$ can win by forcing the game away from $t$.

We proceed to prove our positive results, namely that bidding games are determined when the information according to which tie-breaking is determined does not include the occurrence of ties. Formally, we define a subclass of tie-breaking transducers. {defi} A transducer is un-aware of ties when its alphabet is $V\times\{1,2\}\times\mathbb{N}$, where a letter $\langle v,i,b\rangle\in V\times\{1,2\}\times\mathbb{N}$ means that the token is placed on $v$, Player $i$ wins the bidding, and his winning bid is $b$.

We start with the following lemma that applies to any tie-breaking mechanism. Recall that rows represent Player $1$ bids, columns represent Player $2$ bids, entries on the top-left to bottom-right diagonal represent ties in the bidding, entries above it represent Player $2$ wins, and entries below represent Player $1$ wins.

Lemma 6**.**

Consider a bidding game ${\mathcal{G}}$ with some tie-breaking mechanism $T$ and consider a configuration $c=\langle v,B_{1},B_{2},s\rangle$. Entries in $M_{c}$ in a column above the diagonal are all equal, thus for bids $b_{2}>b_{1},b^{\prime}_{1}$, the entries $\langle b_{1},b_{2}\rangle$ and $\langle b^{\prime}_{1},b_{2}\rangle$ in $M_{c}$ are equal. Also, the entries in a row to the left of the diagonal are equal, thus for bids $b_{1}>b_{2},b^{\prime}_{2}$, the entries $\langle b_{1},b_{2}\rangle$ and $\langle b_{1},b^{\prime}_{2}\rangle$ in $M_{c}$ are equal.

Proof 4.2**.**

Suppose Player $2$ bids $b_{2}$. For $b_{1},b^{\prime}_{1}<b_{2}$, no matter whether Player $1$ bids $b_{1}$ or $b^{\prime}_{1}$, Player $2$’s budget decreases by $b_{2}$, thus both the intermediate states $\langle c,b_{1},b_{2}\rangle$ and $\langle c,b^{\prime}_{1},b_{2}\rangle$ are owned by Player $2$ and have the same neighbors. It follows that $\langle c,b_{1},b_{2}\rangle$ is winning for Player $2$ iff $\langle c,b^{\prime}_{1},b_{2}\rangle$ is winning for Player $2$. The other part of the lemma is dual.

The next lemma relates an entry on the diagonal with its neighbors.

Lemma 7**.**

Consider a bidding game ${\mathcal{G}}$ in which tie-breaking is resolved according to a transducer $T$ that is un-aware of ties. Consider a configuration $c=\langle v,B_{1},B_{2},s\rangle$. Let $b\in\mathbb{N}$. If $\Gamma(s)=1$, i.e., Player $1$ wins ties in $c$, then the entries $\langle b,b\rangle$ and $\langle b,b-1\rangle$ in $M_{c}$ are equal. Dually, if $\Gamma(s)=2$, then the entries $\langle b,b\rangle$ and $\langle b-1,b\rangle$ in $M_{c}$ are equal.

Proof 4.3**.**

We prove for $\Gamma(s)=1$, and the other case is dual. Let $c=\langle v,B_{1},B_{2},s\rangle$. Note that the neighbors of the intermediate vertices $\langle c,b,b\rangle$ and $\langle c,b,b-1\rangle$ are the same. Indeed, Player $1$ is the winner of the bidding in both case, and so his budget decreases by $b$. Also, the update to the state $s$ in $T$ is the same in both cases since $T$ is un-aware of ties. It follows that $\langle c,b,b\rangle$ is winning for Player $1$ iff $\langle c,b,b-1\rangle$ is winning for Player $1$.

We continue to prove our positive results.

Theorem 8**.**

Consider a tie-breaking transducer $T$ that is un-aware of ties. Then, a Müller bidding game that resolves ties using $T$ is determined.

Proof 4.4**.**

We show that transducers that are not aware of ties admit local determinacy, and the theorem follows from Theorem 4. See a depiction of the proof in Figure 6.

Consider a bidding game $\langle V,E,\alpha,N,T\rangle$, where $T$ is un-aware of ties, and consider a configuration vertex $c=\langle v,B_{1},B_{2},s\rangle$. We show that $M_{c}$ either has a $1$-row or a $2$-column. We prove for $\Gamma(s)=1$ and the proof for $\Gamma(s)=2$ is similar. Let $B=\min\{B_{1},B_{2}\}$. When $B_{2}>B_{1}$, the matrix $M_{c}$ is a rectangle. Still the diagonal of interest models biddings that result in ties and it starts from the top left corner of $M_{c}$. The columns $B+1,\ldots,B_{2}$ do not intersect this diagonal. By Lemma 6, the entries in each one of these columns are all equal. We assume all the entries are $1$ as otherwise we find a $2$-column. Similarly, if $B_{1}>B_{2}$, we assume that the entries in the rows $B+1,\ldots,B_{1}$ below the diagonal are all $2$, otherwise we find a $1$-row.

We restrict attention to the $B\times B$ top-left sub-matrix of $M_{c}$. Consider the $B$-th row in $M_{c}$. By Lemma 6, entries in this row that are below the diagonal are all equal, and, since $\Gamma(s)=1$, they also equal the entry on the diagonal. If all entries equal $1$, then together with the assumption above that entries to the right of the diagonal are all $1$, we find a $1$-row. Thus, we assume all entries below and on the diagonal in the $B$-th row all equal $2$. Now, consider the $B$-th column. By Lemma 6, the entries above the diagonal are all equal. If they all equal $2$, together with the entry $\langle B,B\rangle$ on the diagonal and the entries below it, which we assume are all $2$, we find a $2$-column. Thus, we assume the entries in the $B$-th column above the diagonal are all $1$. Next, consider the $(B-1)$-row. Similarly, the elements on and to the left of the diagonal are all equal, and if they equal $1$, we find a $1$-row, thus we assume they are all $2$. We continue in a similar manner until the entry $\langle 1,1\rangle$. If it is $1$, we find a $1$-column and if it is $2$, we find a $2$-row, and we are done.

We conclude this section by relating the computational complexity of bidding games with turn-based games. Let $\text{TB}_{\alpha}$ be the class of turn-based games with a qualitative objective $\alpha$. Let $\text{BID}_{\alpha,\text{trans}}$ be the class of bidding games with transducer-based tie-breaking and objective $\alpha$. The problem TB-WINα gets a game ${\mathcal{G}}\in\text{TB}_{\alpha}$ and a vertex $v$ in ${\mathcal{G}}$, and the goal is to decide whether Player $1$ can win from $v$. Similarly, the problem BID-WIN${}_{\alpha,\text{trans}}$ gets as input a game ${\mathcal{G}}\in\text{BID}_{\alpha,\text{trans}}$ with budgets expressed in unary and a configuration $c$ in ${\mathcal{G}}$, and the goal is to decide whether Player $1$ can win from $c$.

Theorem 9**.**

For a qualitative objective $\alpha$, the complexity of TB-WINα and BID-WIN${}_{\alpha,\text{trans}}$ coincide when the budgets are given in unary.

Proof 4.5**.**

In order to decide whether Player $1$ wins in a configuration $c$ in ${\mathcal{G}}\in\text{BID}_{\alpha,\text{trans}}$, we construct the turn-based game ${\mathcal{G}}_{1}$ in which Player $1$ reveals his bids before Player $2$ and solve ${\mathcal{G}}_{1}$. The determinacy of ${\mathcal{G}}$ implies that if Player $1$ does not win ${\mathcal{G}}_{1}$, the Player $2$ wins ${\mathcal{G}}_{2}$. The size of ${\mathcal{G}}_{1}$ is polynomial in ${\mathcal{G}}$ since the budgets are given in unary.

The other direction is simple: given a turn-based game ${\mathcal{G}}$, we set the total budgets to [math], thus all bids result in ties. The tie-breaking transducer resolves ties by declaring the winner in a vertex $v$ to be Player $i$ if he controls $v$ in ${\mathcal{G}}$. Clearly, the winner in ${\mathcal{G}}^{\prime}$ coincides with the winner in ${\mathcal{G}}$.

5. Random-Based Tie Breaking

In this section we show that bidding games with random-based tie-breaking are determined. A stochastic concurrent game is ${\mathcal{G}}=\langle A,V,\lambda,\delta,\alpha\rangle$ is the same as a concurrent game only that the transition function is stochastic, thus given $v\in V$ and $a^{1},a^{2}\in A$, the transition function $\delta(v,a^{1},a^{2})$ is a probability distribution over $V$. Two strategies $\sigma_{1}$ and $\sigma_{2}$ give rise to a probability distribution $D(\sigma_{1},\sigma_{2})$ over infinite plays.

Traditionally, determinacy in stochastic concurrent games states that each vertex is associated with a value, which is the probability that Player $1$ wins under optimal play [29]. The value is obtained, however, when the players are allowed to use probabilistic strategies. We show a stronger form of determinacy in bidding games; namely, we show that the value exists even when the players are restricted to use deterministic strategies.

{defi}

[Determinacy in stochastic games] Consider a stochastic concurrent game ${\mathcal{G}}$ and a vertex $v\in V$. Let $P_{1}$ and $P_{2}$ denote the set of pure strategies for Players $1$ and $2$, respectively. For $i\in\{1,2\}$, the value for Player $i$, denoted $val_{i}({\mathcal{G}},v)$, is intuitively obtained when he reveals his strategy before the other player. We define $val_{1}({\mathcal{G}},v)=\sup_{\sigma_{1}\in P_{1}}\inf_{\sigma_{2}\in P_{2}}\Pr_{\pi\sim D(\sigma_{1},\sigma_{2})}[\pi\in\alpha]$ and $val_{2}({\mathcal{G}},v)=\inf_{\sigma_{2}\in P_{2}}\sup_{\sigma_{1}\in P_{1}}\Pr_{\pi\sim D(\sigma_{1},\sigma_{2})}[\pi\in\alpha]$. We say that ${\mathcal{G}}$ is determined in $v$ if $val_{1}({\mathcal{G}},v)=val_{2}({\mathcal{G}},v)$ in which case we denote the value by $val({\mathcal{G}},v)$. We say that ${\mathcal{G}}$ is determined if it is determined in all vertices. ∎

The key idea in the proof shows determinacy for reachability games that are played on directed acyclic graphs (DAGs, for short). The following lemma shows that the proof for DAGs implies the general case by following an “unwinding” argument similar to the one used in the value iteration algorithm.

Lemma 10**.**

Determinacy of reachability bidding games that are played on DAGs implies determinacy of general reachability bidding games.

Proof 5.1**.**

Let ${\mathcal{G}}$ be a reachability bidding game with random-based tie breaking and consider a configuration $c$. We claim that $val_{1}({\mathcal{G}},c)=val_{2}({\mathcal{G}},c)$. For $i\in\{1,2\}$, recall that $G_{i}$ is the turn-based stochastic game in which Player $i$ reveals his bid first in each turn. Trivially, Player $i$’s value in ${\mathcal{G}}_{i}$ at $c$ is $val({\mathcal{G}}_{i},c)$. For $n\in\mathbb{N}$, let ${\mathcal{G}}^{n}(c)$ denote the game that starts from $c$ and in which Player $1$ wins iff he reaches the target within $n$ turns. It follows from [23] that the values of ${\mathcal{G}}^{n}_{i}(c)$ converge to the value of ${\mathcal{G}}_{i}$ at $c$, thus val({\mathcal{G}}_{i},c)=\lim_{n\to\infty}val\big{(}{\mathcal{G}}^{n}_{i},(c)\big{)}.

Note that ${\mathcal{G}}^{n}(c)$ is a game that is played on a DAG; indeed, the game ends after at most $n$ turns. The game ${\mathcal{G}}^{n}_{i}(c)$ is the game in which Player $i$ reveals his bid first in each step. The assumption on determinacy of games played on DAGs implies that val\big{(}{\mathcal{G}}^{n}_{1}(c)\big{)}=val\big{(}{\mathcal{G}}^{n}_{2}(c)\big{)}. It thus follows that $val({\mathcal{G}}_{1},c)=val({\mathcal{G}}_{2},c)$ since all the elements in the sequence are equal.

We continue to show determinacy in bidding games on DAGs.

Lemma 11**.**

Reachability bidding games with random-based tie-breaking that are played on DAGs are determined.

Proof 5.2**.**

Consider a reachability game ${\mathcal{G}}$ that is played on a DAG with two distinguished vertices $t_{1}$ and $t_{2}$, which are sinks. There are no other cycles in ${\mathcal{G}}$, thus all plays end either in $t_{1}$ or $t_{2}$, and, for $i\in\{1,2\}$, Player $i$ wins iff the game ends in $t_{i}$. The height of ${\mathcal{G}}$ is the length of the longest path from some vertex to either $t_{1}$ or $t_{2}$. We prove that ${\mathcal{G}}$ is determined by induction on its height. For a height of [math], the claim clearly holds since for every $B_{1},B_{2}\in\mathbb{N}$, the value in $t_{1}$ is $1$ and the value in $t_{2}$ is [math]. Suppose the claim holds for games of heights of at most $n-1$ and we prove for games of height $n$.

Consider a configuration vertex $c=\langle v,B_{1},B_{2}\rangle$ of height $n$. Let $c^{\prime}$ be a configuration vertex that, skipping intermediate vertices, is a neighbor of $c$. Then, the height of $c^{\prime}$ is less than $n$ and by the induction hypothesis, its value is well defined. It follows that the value of the intermediate vertices following $c$ are also well-defined: if the intermediate vertex is controlled by Player $1$ or Player $2$, the value is respectively the maximum or minimum of its neighbors, and if it is controlled by Nature, the value is the average of its two neighbors.

We claim that ${\mathcal{G}}$ is determined in $c$ by showing that one of the players has a (weakly) dominant bid from $c$, where a bid $b_{1}$ dominates a bid $b^{\prime}_{1}$ if, intuitively, Player $1$ always prefers bidding $b_{1}$ over $b^{\prime}_{1}$. It is convenient to consider a variant of the bidding matrix $M_{c}$ of $c$, which is a $(B_{1}+1)\times(B_{2}+1)$ matrix with entries in $[0,1]$, where an entry $M_{c}(b_{1},b_{2})$ represents the value of the intermediate vertex $\langle c,b_{1},b_{2}\rangle$. Note that Player $1$, the reachability player, aims to maximize the value while Player $2$ aims to minimize it. We observe some properties of the entries in $M_{c}$ (see Fig. 6).

• •

An entry on the diagonal is the average of two of its neighbors, namely M_{c}(b,b)=\frac{1}{2}\big{(}M_{c}(b-1,b)+M_{c}(b,b-1)\big{)}.

• •

As in Lemma 6, the entries in a column above the diagonal as well as entries in a row to the left of the diagonal, are all equal.

• •

For $b_{1}>b^{\prime}_{1}>b_{2}$, we have $M_{c}(b_{1},b_{2})\leq M_{c}(b^{\prime}_{1},b_{2})$, since Player $1$ can use the same strategies from $\langle c,b^{\prime}_{1},b_{2}\rangle$ as from $\langle c,b_{1},b_{2}\rangle$. Similarly, for $b_{2}>b^{\prime}_{2}>b_{1}$, we have $M_{c}(b_{1},b_{2})\geq M_{c}(b_{1},b^{\prime}_{2})$.

We show that one of the players has a weakly dominant bid from $c$, where a bid $b_{1}$ dominates a bid $b^{\prime}_{1}$ if for every bid $b_{2}$ of Player $2$, we have $M_{c}(b_{1},b_{2})\geq M_{c}(b^{\prime}_{1},b_{2})$, and dually for Player $2$. Consider the bids [math] and $1$ for the two players. We claim that there is a player for which either [math] weakly dominates $1$ or vice versa. Assume towards contradiction that this is not the case. Consider the $2\times 2$ top-left sub-matrix of $M_{c}$ and denote its values $v_{0,0},v_{0,1},v_{1,0}$, and $v_{1,1}$. Since $v_{1,1}$ is the average of $v_{0,1}$ and $v_{1,0}$, we either have $v_{0,1}\leq v_{1,1}\leq v_{1,0}$ or $v_{0,1}\geq v_{1,1}\geq v_{1,0}$. Suppose w.l.o.g. that the first holds, thus $v_{0,1}\leq v_{1,0}$. Note that $v_{0,0}<v_{0,1}$, since otherwise the bid $1$ dominates [math] for Player $2$. Also, we have $v_{0,0}>v_{1,0}$, since otherwise [math] dominates $1$ for Player $1$. Combining, we have that $v_{0,1}>v_{1,0}$, and we reach a contradiction.

Suppose Player $1$ has a dominating row and the case of Player $2$ is dual. To apply the inductive argument, we show two properties: (1) if row [math] dominates row $1$, then row [math] dominates every other row $i$, and (2) if row $1$ dominates row [math], then column $1$ dominates column [math] without the first two elements. Property (1) implies that if row [math] dominates row $1$, we find a pair of optimal strategies by setting Player $1$’s bid to be [math] and Player $2$’s bid to be a best response to Player $1$’s bid. Property (2) gives rise to a second inductive argument on the size of $M_{c}$; namely, if row $1$ dominates row [math], we can construct a restricted game with the same properties as the original game by removing the first column and row from $M_{c}$. In the case that row $1$ always dominates row [math], there are two cases. If the players’ budgets are equal, we will end up with a matrix that consists of a unique entry. If Player $1$’s budget is larger than Player $2$’s budget, then we end up with a sub-matrix $M^{\prime}_{c}$ that consists of rows that do not intersect the main diagonal of $M_{c}$, thus the entries in a row $i$ in $M^{\prime}_{c}$ are all equal and are larger than those in row $i+1$. Likewise when Player $2$’s budget is larger than Player $1$’s budget. In both cases, one of the players has a weakly dominant strategy.

We conclude the proof by proving the two properties above. We start with Property (1). Assume row [math] dominates row $1$. We show that, for $i\geq 1$, row $i$ dominates row $i+1$. Recall that below the diagonal, for every $i\geq 1$ and $j<i$, we have $v_{i,j}\geq v_{i+1,j}$, and above the diagonal, for $j>i$, we have $v_{i,j}=v_{i-1,j}$. We are left with two claims to show; namely, that $v_{i,i}\geq v_{i+1,i}$ and $v_{i,i+1}\geq v_{i+1,i+1}$. Recall that below the diagonal, for $j<i-1$, we have $v_{i,j}=v_{i,j+1}$. Thus, proceeding down from $v_{0,1}$ and then proceeding right, we obtain $v_{0,1}\leq v_{i+1,i}$. Similarly, above the diagonal, by proceeding right from $v_{0,1}$ and then down, we obtain $v_{0,1}\leq v_{i,i+1}$. Since $v_{1,1}=\frac{1}{2}(v_{0,1}+v_{1,0})$ and we assume that $v_{0,1}\geq v_{1,1}$, we have $v_{0,1}\geq v_{1,0}$. Combining the above with $v_{i+1,i+1}=\frac{1}{2}(v_{i,i+1}+v_{i+1,i})$, we obtain $v_{i+1,i}\leq v_{i+1,i+1}\leq v_{i,i+1}$. Observing the previous entry on the diagonal, we note that the same proof shows that $v_{i,i-1}\leq v_{i,i}\leq v_{i-1,i}$. Thus, from $v_{i,i}$, we take one step left, one step down, and one step to the right and obtain $v_{i,i}\geq v_{i,i-1}\geq v_{i+1,i-1}=v_{i+1,i}$, and we are done.

We proceed to prove Property (2). Assume row $1$ dominates row [math]. As in the above, we have $v_{1,0}\geq v_{1,1}$. Below the diagonal, for every $i\geq 1$, we have $v_{i,0}=v_{i,1}$.

Combining the two theorems above, we obtain the following.

Theorem 12**.**

Reachability bidding games with random-based tie breaking are determined.

6. Advantage-Based Tie-Breaking

Recall that in advantage-based tie-breaking, one of the players holds the advantage, and when a tie occurs, he can choose whether to win and pass the advantage to the other player, or lose the bidding and keep the advantage. Advantage-based tie-breaking was introduced and studied in [21], where determinacy for reachability games was obtained by showing that each vertex $v$ in the game has a threshold budget $\texttt{Thresh}(v)\in(\mathbb{N}\times\{*\})$ such that that Player $1$ wins from $v$ iff his budget is at least $\texttt{Thresh}(v)$, where $n^{*}\in(\mathbb{N}\times\{*\})$ means that Player $1$ wins when he starts with a budget of $n$ as well as the advantage. We show that advantage-based tie-breaking admits local determinacy, thus Müller bidding games with advantage-based tie-breaking are determined.

Recall that the state of the advantage-based tie-breaking mechanism represents which player has the advantage, thus it is in $\{1,2\}$. {lemC}[[21]]

Consider a reachability bidding game ${\mathcal{G}}$ with advantage-based tie-breaking.

• •

Holding the advantage is advantageous: For $i\in\{1,2\}$, if Player $i$ wins from a configuration vertex $\langle v,B_{1},B_{2},-\!i\rangle$, then he also wins from $\langle v,B_{1},B_{2},i\rangle$.

• •

The advantage can be replaced by a unit of budget: Suppose Player $1$ wins in $\langle v,B_{1},B_{2},1\rangle$, then he also wins in $\langle v,B_{1}+1,B_{2}-1,2\rangle$. Suppose Player $2$ wins in $\langle v,B_{1},B_{2},2\rangle$, then he also wins in $\langle v,B_{1}-1,B_{2}+1,1\rangle$.

We need two more observations on the bidding matrix, which are depicted in Figs. 8 and 8, and stated in Lemmas 13 and 14.

Lemma 13**.**

Consider a reachability bidding game ${\mathcal{G}}$ with advantage-based tie-breaking. Consider a configuration $c=\langle v,B_{1},B_{2},1\rangle$ in ${\mathcal{G}}$, where Player $1$ has the advantage, and $i\in\{0,\ldots,B_{1}\}$. Then,

• •

If $M_{c}(i-1,i)=M_{c}(i,i-1)=2$, then $M_{c}(i,i)=2$.

• •

If $M_{c}(i,i)=2$, then $M_{c}(i+1,i)=2$.

Proof 6.1**.**

We start with the first claim. Since both players bid $i$, a tie occurs. Since Player $1$ holds the advantage, there are two cases. In the first case, Player $1$ calls himself the winner and proceeds to a configuration $\langle v^{\prime},B_{1}-i,B_{2}+i,2\rangle$. We assume Player $2$ wins from the vertex $\langle c,i,i-1\rangle$, in which he loses the first bidding. A possible choice of vertex for Player $1$ is $v^{\prime}$, thus Player $2$ wins from the resulting configuration $\langle v^{\prime},B_{1}-i,B_{2}+i,1\rangle$. By Lemma 6, Player $2$ also wins $\langle v^{\prime},B_{1}+i,B_{2}-i,2\rangle$. In the second case, Player $1$ calls Player $2$ the winner. We assume Player $2$ wins from the vertex $\langle c,i-1,i\rangle$, in which he wins the first bidding. Let $v^{\prime}$ be the choice of vertex in a winning strategy, thus the resulting configuration is $\langle v^{\prime},B_{1}-i,B_{2}+i,1\rangle$, which is winning for Player $2$ and is the resulting configuration when Player $2$ chooses $v^{\prime}$ following the tie.

For the second claim, we assume Player $2$ wins in $\langle c,i,i\rangle$, the vertex that represents a bidding tie. Since Player $1$ has the tie-breaking advantage, Player $2$ wins in particular when Player $1$ calls himself the winner, and the resulting configuration is $\langle v^{\prime},B_{1}-i,B_{2}+i,2\rangle$. We claim that Player $2$ wins from $\langle c,i+1,i\rangle$, thus Player $1$ wins the bidding. Let $\langle v^{\prime},B_{1}-(i+1),B_{2}+(i+1),1\rangle$ be the resulting configuration, which by Lemma 6, is a Player $2$ winning vertex.

Lemma 14**.**

Consider a reachability bidding game ${\mathcal{G}}$ with advantage-based tie-breaking. Consider a configuration $c=\langle v,B_{1},B_{2},2\rangle$ in ${\mathcal{G}}$, where Player $2$ has the advantage, and $i\in\{0,\ldots,B_{2}\}$. Then,

• •

If $M_{c}(i-1,i)=M_{c}(i,i-1)=1$, then $M_{c}(i,i)=1$.

• •

If $M_{c}(i-1,i)=2$, then $M_{c}(i,i)=2$.

Proof 6.2**.**

We start with the first claim. Consider a configuration vertex $c=\langle v,B_{1},B_{2},2\rangle$. Since Player $1$ wins when the bids are $i$ and $i-1$, i.e., Player $1$ wins the bidding, there is a configuration vertex $\langle v^{\prime},B_{1}-i,B_{2}+i,2\rangle$ from which Player $1$ wins. Similarly, since Player $1$ wins when the bids are $i-1$ and $i$, he wins no matter which vertex $v^{\prime\prime}$ Player $2$ chooses to move to, i.e., from configurations of the form $\langle v^{\prime\prime},B_{1}+i,B_{2}-i,2\rangle$. Consider the case that both players bid $i$. Player $2$ has the tie-breaking advantage, thus there are two cases to consider. First, Player $2$ calls himself the winner and chooses the next vertex, thus the proceeding configuration is of the form $\langle v^{\prime\prime},B_{1}+i,B_{2}-i,1\rangle$. Combining the above with Lemma 6, Player $1$ wins. Second, Player $2$ calls Player $1$ the winner of the bidding. Player $1$ then chooses $v^{\prime}$ as in the above, and the following configuration is $\langle v^{\prime}B_{1}-i,B_{2}+i,2\rangle$, from which Player $1$ wins.

We continue to the second part of the lemma. Consider the outcome $c^{\prime}$ in which Player $1$ bids $i-1$ and Player $2$ bids $i$. Player $2$’s budget increases by $i-1$ and he keeps the advantage. On the other hand, consider the outcome $c^{\prime\prime}$ in which both players bid $i$ and Player $2$ calls Player $1$ the winner. Here, Player $2$’s budget increases by $i$ and the advantage is transferred to Player $1$. By Lemma 6, the advantage can be replaced by a unit of budget. Thus, since Player $2$ wins in $\langle c^{\prime},i-1,i\rangle$, he also wins in $\langle c^{\prime\prime},i,i\rangle$.

We are ready to prove determinacy.

Theorem 15**.**

Müller* bidding games with advantage-based tie-breaking are determined.*

Proof 6.3**.**

Consider a bidding game ${\mathcal{G}}$ with advantage-based tie-breaking and a configuration $c=\langle v,B_{1},B_{2},s\rangle$ in ${\mathcal{G}}$. We make observations on the entries in $M_{c}$ above and below the diagonal similar to Thm. 12. Consider the entries above the diagonal. These represent biddings outcomes in which Player $2$ wins. Fixing a Player $2$ bid $b_{2}$, for any Player $1$ bid $b_{1}<b_{2}$ the outcome of the bidding is the same, i.e., both Player $2$ wins the bidding and the budget update is the same. Thus, entries in a column above the diagonal are all equal. Also, as we proceed right above the diagonal, Player $2$ bids higher and so his updated budget is lower. It follows that if Player $1$ wins in a column $x$, he necessarily wins in every column $x^{\prime}>x$ to its right. Let $x_{2}$ denote the first column above the diagonal all of whose entries are $1$. Dually, below the diagonal, entries in rows are equal and as we proceed down, Player $1$’s updated budget is lower. Thus, there is a row, denoted $x_{1}$, strictly below which all entries are $2$.

We distinguish between two cases according to which player has the advantage in $c$. In the first case, Player $2$ has the advantage in $c$ (see a depiction of the proof in Fig. 9). We distinguish between two sub-cases. In the first case $x_{2}\leq x_{1}$. Consider the row $x_{1}$. By the definitions of $x_{1}$ and $x_{2}$, the entries in the row to the left and to the right of the diagonal are all $1$. In addition, since $x_{2}\leq x_{1}$, the entries in the column $x_{1}$ above the diagonal are also $1$. Thus, by Lemma 14, we have $M_{c}(x_{1},x_{1})=1$ and we find a $1$-row. In the second case $x_{2}>x_{1}$. Observe the column $x_{1}$. By the definitions of $x_{1}$ and $x_{2}$ the entries above and below the diagonal are all $2$ and by Lemma 14, the entry $x_{1}$ entry on the diagonal is also $2$, thus we find a $2$-column.

For the second case, suppose Player $1$ has the advantage (see a depiction of the proof in Fig. 10). We distinguish between three sub-cases. In the first case $x_{2}>x_{1}+1$. Consider the $(x_{1}+1)$ column. By the definition of $x_{1}$ and $x_{2}$, the entries below and above the diagonal are $2$. Since the entries in the row $(x_{1}+1)$ to the left of the diagonal are $2$, by Lemma 13, the diagonal is also $2$, thus the $(x_{1}+1)$-column is a $2$-column. In the second case $x_{2}=x_{1}+1$. We observe the $x_{1}$ element of the diagonal. If it is $1$, the $x_{1}$-row is a $1$-row, and if it is $2$, the $x_{1}$-column is a $2$-column. In the third case $x_{1}\geq x_{2}$. Since we have $M_{c}(x_{1},x_{1}-1)=1$, i.e., the element immediately to the left of the diagonal in the $x_{1}$ row, the contrapositive of Lemma 13 implies that $M_{c}(x_{1}-1,x_{1}-1)=1$. Thus, the $(x_{1}-1)$-row is a $1$-row, and we are done.

We turn to study computational complexity of bidding games. Let $\text{BID}_{\alpha,\text{adv}}$ be the class of bidding games with advantage-based tie-breaking and objective $\alpha$, and let BID-WIN${}_{\alpha,\text{adv}}$ be the respective decision problem. Recall that TB-WINα is the decision problem for turn-based games.

Theorem 16**.**

For a qualitative objective $\alpha$, the complexity of TB-WINα and BID-WIN${}_{\alpha,\text{adv}}$ coincide when the budgets are given in unary.

Proof 6.4**.**

The direction from BID-WIN${}_{\alpha,\text{adv}}$ to TB-WINα follows from determinacy as in Theorem 9. For the other direction, consider a turn-based game ${\mathcal{G}}$ and an initial vertex $v_{0}$. We assume w.l.o.g. that players alternate turns in ${\mathcal{G}}$. That is, the neighbors of a Player $i$ vertex $v$ in ${\mathcal{G}}$ are controlled by Player $-\!i$. We construct a bidding game ${\mathcal{G}}^{\prime}$ in which the total budgets is [math]. We introduce to ${\mathcal{G}}$ two new sink vertices $t_{1}$ and $t_{2}$, where a play that ends in $t_{i}$ is winning for Player $i$, for $i\in\{1,2\}$. For a Player $i$ vertex $v$ in ${\mathcal{G}}$, we add an edge from $v$ to $t_{-\!i}$, thus if Player $i$ has the advantage in $v$, he must use it. Suppose $v_{0}$ is a Player $1$ vertex in ${\mathcal{G}}$. It is not hard to show that Player $1$ wins from $v_{0}$ in ${\mathcal{G}}^{\prime}$ when he has the advantage iff he wins from $v_{0}$ in ${\mathcal{G}}$.

7. Strongly-Connected Games

Reasoning about strongly-connected games is key to the solution in continuous-bidding infinite-duration games [7, 8, 10]. It is shown that in a strongly-connected continuous-bidding game, with every initial positive budget, a player can force the game to visit every vertex infinitely often. It follows that in a strongly-connected Büchi game ${\mathcal{G}}$ with at least one accepting state, Player $1$ wins with every positive initial budget. We show a similar result in discrete-bidding games in two cases.

Theorem 17**.**

Consider a strongly-connected bidding game ${\mathcal{G}}$ in which tie-breaking is either resolved randomly or by a transducer that always prefers Player $1$. Then, for every pair of initial budgets, Player $1$ can force visiting every vertex in ${\mathcal{G}}$ infinitely often with probability $1$.

Proof 7.1**.**

Suppose Player $1$ moves whenever a tie occurs and let $v$ be a vertex in the game. Player $1$ follows a strategy in which he always bids [math] and moves to a vertex that is closer to $v$. For every initial budget of Player $2$, he wins only a finite number of times. Consider the outcome following the last time Player $2$ wins. Since Player $1$ wins all biddings, in each turn the token moves one step closer to $v$, and thus we visit $v$ every $|V|$ turns, in the worst case. Similarly, when tie-breaking is resolved randomly, the game following the last win of Player $2$ is an ergodic Markov chain in which it is well-known that every vertex is visited infinitely often with probability $1$.

In [21], it is roughly stated that, with advantage-based tie-breaking, as the budgets tend to infinity, the game “behaves” similarly to a continuous-bidding game. The following theorem shows, however, that infinite-duration discrete-bidding games can be quite different from their continuous counterparts.

Theorem 18**.**

There is a Büchi game such that with any pair of initial budgets, Player $1$ wins under continuous-bidding and loses under discrete-bidding.

Proof 7.2**.**

Consider the game that is depicted in Fig. 11 with the initial vertex $v_{1}$. Since the game is strongly-connected and it has an accepting vertex, by [7], Player $1$ wins under continuous bidding with any positive initial budget. We proceed to study the game under discrete bidding. Suppose Player $1$’s budget is $B_{1}\in\mathbb{N}$ and assume wlog that Player $2$’s budget is [math] (Player $2$ can always ignore excess funds and play as if his initial budget is [math]). Player $2$ always bids [math], uses the advantage when he has it, and, upon winning, stays in $v_{1}$ and moves from $v_{2}$ to $v_{1}$. Note that in order to visit $v_{3}$, Player $1$ needs to win two biddings in a row; in $v_{1}$ and $v_{2}$. Thus, in order to visit $v_{3}$, he must “invest” a unit of budget, meaning that the number of visits to $v_{3}$ is bounded by $B_{1}$, and in particular Player $1$ cannot force infinite many visits to $v_{3}$, thus he loses the game.

8. Discussion and Future Work

We study discrete-bidding infinite-duration bidding games and identify large fragments of bidding games that are determined. Bidding games are a subclass of concurrent games. We are not aware of other subclasses of concurrent games that admit determinacy. We find it an interesting future direction to extend the determinacy we show here beyond bidding games. Weaker versions of determinacy in fragments of concurrent games have been previously studied [39].

We focused on bidding games with “Richman” bidding, i.e., the winner of the bidding pays the other player, and it is interesting to study other bidding games with other bidding rules. Bidding reachability games with all-pay bidding in which both players pay their bid to the bank were studied with continuous bidding [11] as well as with discrete Richman-all-pay bidding [32] in which both players pay their bid to the other player. In addition, it is interesting to study discrete-bidding games with quantitative objectives and non-zero-sum games, which were previously studied only for continuous bidding [7, 8, 31].

This work belongs to a line of works that transfer concepts and ideas between the areas of formal verification and algorithmic game theory [35]. Examples of works in the intersection of the two fields include logics for specifying multi-agent systems [2, 18, 33], studies of equilibria in games related to synthesis and repair problems [17, 15, 24, 1], non-zero-sum games in formal verification [19, 14], and applying concepts from formal methods to resource allocation games such as rich specifications [12], efficient reasoning about very large games [6, 26], and a dynamic selection of resources [9].