where the first implication holds because, by definition of $\sigma_{max}$ and $E$, for every $s_1 \cdots s_n \in CS^*$, $\text{supp}(\sigma(s_1 \cdots s_n)) \subseteq \text{supp}(\sigma_{max}(s_1 \cdots s_n))$ while the second impli- cation is from Equation (8.11). Thus $\mathbb{P}_{\delta_L}^{\sigma, \tau}(\text{Safety}) = 1$ and we get $\mathbb{P}_{\delta_L}^{\sigma, \tau'}(\text{Safety}) > 0$ by definition of $\tau'$.

* Or $\mathbb{P}_{\delta_L}^{\sigma, \tau'}(E) < 1$. Then by definition of $E$ there exists $n \in \mathbb{N}$ such that

$$ \mathbb{P}_{\delta_L}^{\sigma, \tau'} (A_n \notin \text{ISafe}_{\mathcal{L}}(\mathcal{R}_{\text{Eve}}^n)) > 0 . $$

By definition of ISafe$_{\mathcal{L}}$ it implies $\mathbb{P}_{\delta_L}^{\sigma, \tau'} (\mathcal{R}_{\text{Eve}}^{n+1} \in \mathcal{L}) > 0$, thus there exists $B \in \mathcal{L}$ such that $\mathbb{P}_{\delta_L}^{\sigma, \tau'} (\mathcal{R}_{\text{Eve}}^{n+1} = B) > 0$. By definition of $\tau'$ we get $\mathbb{P}_{\delta_L}^{\sigma, \tau_{n+1,B}} (\mathcal{R}_{\text{Eve}}^{n+1} = B) > 0$, because whatever finite play $v_0, \dots, v_{n+1}$ leads with positive probability to the event $\{\mathcal{R}_{\text{Eve}}^{n+1} = B\}$, the same finite play can occur with $\tau_{n+1,B}$ since $\tau_{n+1,B}$ plays every possible action for the $n+1$ first steps. Since $\tau_{n+1,B}$ coincides with $\tau_{\text{rand}}$ for the first $n+1$ steps then by definition of beliefs, $\mathbb{P}_{\delta_L}^{\sigma, \tau_{n+1,B}} (\mathcal{R}_{\text{Eve}}^{n+1} = B) > 0$ and $B \subseteq \{k \in K \mid \mathbb{P}_{\delta_L}^{\sigma, \tau_{n+1,B}} (K_{n+1} = k \mid \mathcal{R}_{\text{Eve}}^{n+1} = B) > 0\}$. Using the definition of $\tau_B$ we get $\mathbb{P}_{\delta_L}^{\sigma, \tau_{n+1,B}} (\text{CoBuchi}) > 0$.

As a consequence by definition of $\tau'$ we get $\mathbb{P}_{\delta_L}^{\sigma, \tau'} (\text{CoBuchi}) > 0$.

In both cases, for every $\sigma$, $\mathbb{P}_{\delta_L}^{\sigma, \tau'} (\text{CoBuchi}) > 0$ thus $\tau'$ is positively winning from $L$. This contradicts the hypothesis $L \in \mathcal{L}_{\text{Eve},=1}$. As a consequence we get Equation (8.10) by contradiction.

Using Equation (8.10), we apply Lemma 124 to the collection $\mathcal{L}_{\text{Adam},>0}$ and the strategy $\sigma_{max}$. The collection $\mathcal{L}_{\text{Adam},>0}$ is downward-closed because $\mathcal{L}_{\text{Adam},>0}$ is upward-closed: if a support is positively winning for Adam then any greater support is positively winning as well, using the same positively winning strategy.

Thus $\sigma_{max}$ is almost-surely winning for the Büchi game from every support in $\mathcal{L}_{\text{Adam},>0}$ i.e. every support which is not positively winning for Adam, hence the game is qualitatively determined.

### 8.3.5 Decidability: proof of Theorem 97 and Theorem 98

#### A naïve algorithm

As a corollary of the proof of qualitative determinacy (Theorem 96), we get a maximal strategy $\sigma_{max}$ for player 1 (see Definition 27) to win almost-surely Büchi games.

**Corollary 19.** If player 1 has an almost-surely winning strategy in a Büchi game with observable actions then the maximal strategy $\sigma_{max}$ is almost-surely winning.

A simple algorithm to decide for which player a game is winning can be derived from Corollary 19: this simple algorithm enumerates all possible belief strategies and test each one of them to see if it is almost-surely winning. The test reduces to checking positive winning in one-player co-Büchi games and can be done in exponential time.
As there is a doubly exponential number of belief strategies, this can be done in time doubly exponential. This algorithm also appears in [GS09b]. This settles the upper bound for Theorem 97.

Matching complexity lower bounds are established in [BGG17], proving that this enumeration algorithm is optimal for worst case complexity. While optimal in the worst case, this algorithm is likely to be inefficient in practice. For instance, if player 1 has no almost-surely winning strategy, then this algorithm will enumerate every single of the doubly exponential many possible belief strategies. Instead, we provide fixed point algorithms which do not enumerate every possible strategy in Theorem 99 for reachability games and Theorem 100 for Büchi games. Although they should perform better on games with particular structures, these fixed point algorithms still have a worst-case 2-EXPcomplexity.

## A fixed point algorithm for reachability games

We turn now to the (fixed points) algorithms which compute the set of supports that are almost-surely or positively winning for various objectives.

**Theorem 99 (Deciding positive winning in reachability games).** In a reachability game each initial distribution $\delta$ is either positively winning for player 1 or surely winning for player 2, and this depends only on $\text{supp}(\delta) \subseteq V$. The corresponding partition of $\mathcal{P}(V)$ is computable in time $\mathcal{O}(|G| \cdot 2^{|V|})$, where $|G|$ denotes the size of the description of the game, as the largest fixed point of a monotonic operator $\Phi: \mathcal{P}(\mathcal{P}(V)) \to \mathcal{P}(\mathcal{P}(V))$ computable in time linear in $|G|$.

We denote $\text{TT}$ the set of vertices whose colour is 1.

*Proof.* Let $\mathcal{L}_\infty \subseteq \mathcal{P}(V \setminus TT)$ be the greatest fixed point of the monotonic operator $\Phi: \mathcal{P}(\mathcal{P}(V \setminus TT)) \to \mathcal{P}(\mathcal{P}(V \setminus TT))$ defined by:

$$ \Phi(\mathcal{L}) = \{L \in \mathcal{L} \mid \exists j_L \in J, \forall d \in T, (a_2(d) = j_L) \implies (\mathcal{B}_{\text{Adam}}(L, d) \in \mathcal{L} \cup \{\emptyset\})\}, \quad (8.12) $$

in other words $\Phi(\mathcal{L})$ is the set of supports such that player 2 has an action which ensure his next belief will be in $\mathcal{L}$, whatever signal $d$ he might receive. Let $\sigma_{\text{rand}}$ be the strategy for player 1 that plays randomly any action.

We are going to prove that:

1. every support in $\mathcal{L}_\infty$ is surely winning for player 2,

2. and $\sigma_{\text{rand}}$ is positively winning from any support $L \subseteq V$ which is not in $\mathcal{L}_\infty$.

We start with proving the first item. To win surely from any support $L \in \mathcal{L}_\infty$, player 2 uses the following belief strategy $\tau_B$: when the current belief of player 2 is $L \in \mathcal{L}_\infty$ then player 2 plays an action $j_L$ defined as in Equation (8.12). By definition of $\Phi$ and since $\mathcal{L}_\infty$ is a fixed point of $\Phi$, there always exists such an action. When playing with the belief strategy $\tau_B$, starting from a support in $\mathcal{L}_\infty$, the beliefs of player 2 stay in $\mathcal{L}_\infty$ and never intersect $\text{TT}$ because $\mathcal{L}_\infty \subseteq \mathcal{P}(V \setminus \text{TT})$. According to Equation (8.3) of beliefs (Lemma 124), this guarantees the play never visits $\text{TT}$, whatever strategy is used by player 1.
We now prove the second item. Let $\mathcal{L}_0 = \mathcal{P}(V \setminus TT) \supseteq \mathcal{L}_1 = \Phi(\mathcal{L}_0) \supseteq \mathcal{L}_2 = \Phi(\mathcal{L}_1) \dots$ and $\mathcal{L}_\infty$ be the limit of this sequence, the greatest fixed point of $\Phi$. We prove that for any support $L \in \mathcal{P}(V)$, if $L \notin \mathcal{L}_\infty$ then:

$$ \sigma_{\text{rand}} \text{ is positively winning for player 1 from } L. \qquad (8.13) $$

If $L \cap TT \neq \emptyset$, Equation (8.13) is obvious. To deal with the case where $L \cap TT = \emptyset$, we define for every $n \in \mathbb{N}$, $\mathcal{H}_n = \mathcal{P}(V \setminus TT) \setminus \mathcal{L}_n$, and we prove by induction on $n \in \mathbb{N}$ that for every $L \in \mathcal{H}_n$, for every initial distribution $\delta_L$ with support $L$, for every behavioral strategy $\tau$,

$$ \mathbb{P}_{\delta_L}^{\sigma_{\text{rand}}, \tau} (\exists m, 2 \le m \le n+1, V_m \in TT) > 0. \qquad (8.14) $$

For $n=0$, Equation (8.14) is obvious because $\mathcal{H}_0 = \emptyset$. Suppose that for some $n \in \mathbb{N}$, Equation (8.14) holds for every $L' \in \mathcal{H}_n$, and let $L \in \mathcal{H}_{n+1} \setminus \mathcal{H}_n$. Then by definition of $\mathcal{H}_{n+1}$,

$$ L \in \mathcal{L}_n \setminus \Phi(\mathcal{L}_n) . \qquad (8.15) $$

Let $\delta_L$ be an initial distribution with support $L$ and $\tau$ any behavioral strategy for player 2. Let $J_0 \subseteq J$ be the support of $\tau(\delta_L)$ and $j_L \in J_0$. According to Equation (8.15), by definition of $\Phi$, there exists a signal $d \in D$ such that $a_2(d) = j_L$ and $\mathcal{B}_{\text{Adam}}(L, d) \notin \mathcal{L}_n$ and $\mathcal{B}_{\text{Adam}}(L, d) \neq \emptyset$. According to Equation (8.3) of beliefs (Lemma 124), $\forall k \in \mathcal{B}_{\text{Adam}}(L, d), \mathbb{P}_{\delta_L}^{\sigma_{\text{rand}}, \tau}(V_2 = k \wedge D_1 = d) > 0$. If $\mathcal{B}_{\text{Adam}}(L, d) \cap TT \neq \emptyset$ then according to the definition of beliefs, $\mathbb{P}_{\delta_L}^{\sigma_{\text{rand}}, \tau}(V_2 \in TT) > 0$. Otherwise $\mathcal{B}_{\text{Adam}}(L, d) \in \mathcal{P}(V \setminus TT) \setminus \mathcal{L}_n = \mathcal{H}_n$ hence distribution $\delta_d : k \to \mathbb{P}_{\delta_L}^{\sigma_{\text{rand}}, \tau}(V_2 = k | D_1 = d)$ has its support in $\mathcal{H}_n$. By inductive hypothesis, for every behavioral strategy $\tau'$,

$$ \mathbb{P}_{\delta_d}^{\sigma_{\text{rand}}, \tau'} (\exists m \in \mathbb{N}, 2 \le m \le n+1, V_m \in TT) > 0 $$

hence using the shifting lemma and the definition of $\delta_d$,

$$ \mathbb{P}_{\delta}^{\sigma_{\text{rand}}, \tau} (\exists m \in \mathbb{N}, 3 \le m \le n+2, V_m \in TT) > 0, $$

which completes the proof of the inductive step.

Hence Equation (8.14) holds for every behavioural strategy $\tau$. Thus Equation (8.14) holds as well for every general strategy $\tau$.

To compute the partition of supports between those positively winning for player 1 and those surely winning for player 2, it is enough to compute the largest fixed point of $\Phi$. Since $\Phi$ is monotonic, and each application of the operator can be computed in time linear in the size of the game ($|G|$) and the number of supports ($2^{|V|}$) the overall computation can be achieved in time $|G| \cdot 2^{|V|}$. To compute the strategy $\tau_B$, it is enough to compute for each $L \in \mathcal{L}_\infty$ one action $j_L$ such that $(a_2(d) = j_L) \implies (\mathcal{B}_{\text{Adam}}(L, d) \in \mathcal{L}_\infty)$. $\square$

As a byproduct of the proof one obtains the following bounds on time and probabilities before reaching a target state, when player 1 uses the uniform memoryless strategy $\sigma_{\text{rand}}$. From an initial distribution positively winning for the reachability objective, for every strategy $\tau$,

$$ \mathbb{P}_{\delta}^{\sigma_{\text{rand}}, \tau} (\exists n \le 2^{|V|}, C_n = 1) \ge \left( \frac{1}{p_{\min} |A|} \right)^{2^{|V|}}, \qquad (8.16) $$
where $p_{\min}$ is the smallest non-zero transition probability.

## A fixed point algorithm for Büchi games

To decide whether player 1 wins almost-surely a Büchi game, we provide an algorithm which runs in doubly-exponential time. It uses the algorithm for reachability games as a sub-procedure.

**Theorem 100 (Deciding almost-sure winning in Büchi games).** In a Büchi game each initial distribution $\delta$ is either almost-surely winning for player 1 or positively winning for player 2, and this depends only on $\text{supp}(\delta) \subseteq V$. The corresponding partition of $\mathcal{P}(V)$ is computable in time $\mathcal{O}(2^{2^{|G|}})$, where $|G|$ denotes the size of the description of the game, as a projection of the greatest fixed point $\mathcal{L}_{\infty}$ of a monotonic operator

$$ \Psi: \mathcal{P}(\mathcal{P}(V) \times V) \to \mathcal{P}(\mathcal{P}(V) \times V). $$

The operator $\Psi$ is computable using as a nested fixed point the operator $\Phi$ of Theorem 99. The almost-surely winning belief strategy of player 1 and the positively winning 2-belief strategy of player 2 can be extracted from $\mathcal{L}_{\infty}$.

We sketch the main ideas of the proof of Theorem 100.

First, suppose that from every initial support, player 1 can win positively the reachability game. Then she can do so using a belief strategy and according to Lemma 124, this strategy guarantees almost-surely the Büchi condition.

In general though player 1 is not in such an easy situation and there exists a support $L$ which is not positively winning for her for the reachability objective. Then by qualitative determinacy, player 2 has a strategy to achieve surely her safety objective from $L$, which is a fortiori surely winning for her co-Büchi objective as well.

We prove that in case player 2 can force with positive probability the belief of player 1 to be $L$ eventually from another support $L'$, then player 2 has a general strategy to win positively from $L'$. This is not completely obvious because in general player 2 cannot know exactly when the belief of player 1 is $L$ (he can only compute the 2-Belief, letting him know all the possible beliefs player 1 can have). However player 2 can make blind guesses, and be right with $> 0$ probability. For winning positively from $L'$, player 2 plays totally randomly until he guesses randomly that the belief of player 1 is $L$, at that moment he switches to a strategy surely winning from $L$. Such a strategy is far from being optimal, because player 2 plays randomly and in most cases he makes a wrong guess about the belief of player 1. However there is a non zero probability for his guess to be right.

Hence, player 1 should surely avoid her belief to be $L$ or $L'$ if she wants to win almost-surely. However, doing so player 1 may prevent the play from reaching target states, which may create another positively winning support for player 2, and so on. This is the basis of our fixed point algorithm.

Using these ideas, we prove that the set $\mathcal{L}_{\infty} \subseteq \mathcal{P}(V)$ of supports almost-surely winning for player 1 for the Büchi objective is the largest set of initial supports from
which:

player 1 has a strategy which win positively the reachability game
and also ensures at the same time her belief to stay in $\mathcal{L}_{\infty}$. (†)

Property Equation (†) can be reformulated as a reachability condition in a new game whose states are states of the original game augmented with beliefs of player 1, kept hidden to player 2.

The fixed point characterisation suggests the following algorithm for computing the set of supports positively winning for player 2: $\mathcal{P}(V) \setminus \mathcal{L}_{\infty}$ is the limit of the sequence $\emptyset = \mathcal{L}'_0 \subsetneq \mathcal{L}'_0 \cup \mathcal{L}''_1 \subsetneq \mathcal{L}'_0 \cup \mathcal{L}'_1 \subsetneq \mathcal{L}'_0 \cup \mathcal{L}''_1 \cup \mathcal{L}''_2 \subsetneq \dots \subsetneq \mathcal{L}'_0 \cup \dots \cup \mathcal{L}'_m = \mathcal{P}(V) \setminus \mathcal{L}_{\infty}$, where

• from supports in $\mathcal{L}''_{i+1}$ player 2 can surely guarantee the safety objective, under the hypothesis that player 1 guarantees for sure her beliefs to stay outside $\mathcal{L}'_i$,

• from supports in $\mathcal{L}'_{i+1}$ player 2 can ensure with positive probability the belief of player 1 to be in $\mathcal{L}''_{i+1}$ eventually, under the same hypothesis.

The overall strategy of player 2 positively winning for the co-Büchi objective consists in playing randomly for some time until he decides to pick up randomly a belief $L$ of player 1 in some $\mathcal{L}''_i$, bets that the current belief of player 1 is $L$ and that player 1 guarantees for sure her future beliefs will stay outside $\mathcal{L}'_i$. He forgets the signals he has received up to that moment and switches definitively to a strategy which guarantees the first item. With positive probability, player 2 guesses correctly the belief of player 1 at the right moment, and future beliefs of player 1 will stay in $\mathcal{L}'_i$, in which case the co-Büchi condition holds and player 2 wins.

In order to ensure the first item, player 2 makes use of the hypothesis about player 1 beliefs staying outside $\mathcal{L}'_i$. For that player 2 needs to keep track of all the possible beliefs of player 1, hence the doubly-exponential memory. The reason is player 2 can infer from this data structure some information about the possible actions played by player 1: in case for every possible belief of player 1 an action $i \in I$ creates a risk to reach $\mathcal{L}'_i$ then player 2 knows for sure this action is not played by player 1. This in turn helps player 2 to know which are the possible states of the game. Finally, when player 2 estimates the state of the game using his 2-beliefs, this gives a potentially more accurate estimation of the possible states than simply computing his 1-beliefs.

The positively winning 2-belief strategy of player 2 has a particular structure. All memory updates are deterministic except for one: from the initial memory state $\emptyset$, whatever signal is received there is non-zero chance that the memory state stays $\emptyset$ but it may as well be updated to several other memory states.
Part IV

Infinite
<figure><img src="image_69.png" /></figure>
TIMED
GAMES

<figure><img src="image_70.png" /></figure>
Chapter 9

# Timed Games

NICOLAS MARKEY, OCAN SANKUR

The ability to model real-time constraints is crucial when automata and games are used for verification and synthesis. Timed automata [AD94] are a model of choice for reasoning about real-time systems: they extend finite-state automata with a finite number of *clocks*, which are real-valued variables all growing at the same rate, used to measure and constrain the elapse of time between various transitions in the automaton. Because these clocks can take arbitrary non-negative values, the set of configurations of a timed automaton is infinite. Still, reachability (and many other problems) remain decidable in timed automata. The interested reader can find more background in [AD94], but we will try to keep our presentation self-contained.

In this chapter, we consider game models based on timed automata; we call them *timed games* throughout this chapter. In timed games, besides choosing which transitions should be played, the players also decide how much time will elapse before each transition. The elapsed time is determined using clocks, and the edges have guards which determine clock values for which the edge can be taken.

**Example 1.** Figure 9.1 contains a timed game with clock x, where Eve's objective is to reach the vertex G. We will define these arenas as concurrent arenas: dashed edges belong to Adam, and plain edges to Eve. Both players can take any edge at any time as long as the guard is satisfied. For instance, Eve's edge from $ℓ_1$ to $ℓ_2$ is only available if clock x has value at most 1, while Adam's edge from $ℓ_1$ to $ℓ_3$ is available if x is less than 1.

In the next section, we define timed games and their semantics formally. Then we introduce some classical tools needed to reason about the space of clock valuations, and finally present an efficient algorithm for deciding the winner in timed games with reachability objectives.
<figure><img src="image_71.png" /><figcaption>Figure 9.1: Timed game $\mathcal{A}_1$.</figcaption></figure>

## 9.1 Notations

We fix a finite set $\mathcal{C}$ of clock variables to be used in our timed games. Elements of $\mathbb{R}_{\ge 0}^{\mathcal{C}}$, which assign a value to each clock, are called valuations.

Clocks will be used to define clock constraints, which in turn are used in timed automata to restrict the set of allowed behaviours: edges are decorated with clock constraints defining conditions for their availability. An *atomic clock constraint* is a formula of the form $k \le x \le' l$ or $k \le x - y \le' l$ where $x,y \in \mathcal{C}$, $k,l \in \mathbb{Z} \cup \{-\infty, \infty\}$ and $\le, \le' \in \{<, \le\}$. A *clock constraint* is a conjunction of atomic clock constraints. A valuation $v: \mathcal{C} \to \mathbb{R}_{\ge 0}$ satisfies a clock constraint $g$, denoted $v \models g$, if all atomic clock constraints are satisfied when each $x \in \mathcal{C}$ is replaced with its value $v(x)$. We write $\Phi_{\mathcal{C}}$ for the set of clock constraints built on the clock set $\mathcal{C}$.

For a subset $R \subseteq \mathcal{C}$ and a valuation $v$, we denote with $v[R \leftarrow 0]$ the valuation defined by $v[R \leftarrow 0](x) = 0$ if $x \in R$ and $v[R \leftarrow 0](x) = v(x)$ otherwise. Given $d \in \mathbb{R}_{\ge 0}$ and a valuation $v$, the valuation $v+d$ is defined by $(v+d)(x) = v(x)+d$ for all $x \in \mathcal{C}$. We extend these operations to sets of valuations in the obvious way.

We now formally define *timed games*, which are finite representations that define infinite-state, non-stochastic concurrent games.

**Definition 28.** A timed arena $\mathcal{T}$ is a tuple $(\mathcal{L}, \mathcal{C}, E_{Eve}, E_{Adam}, c)$, where $\mathcal{L}$ is a finite set of locations, $\mathcal{C}$ is a finite set of clocks, $E_{Eve}, E_{Adam} \subseteq \mathcal{L} \times \Phi_{\mathcal{C}} \times 2^{\mathcal{C}} \times \mathcal{L}$ are the sets of edges respectively controlled by Eve and Adam, and $c: E_{Eve} \cup E_{Adam} \to C$ is the coloring function. A timed game is a pair $(\mathcal{T}, \Omega)$ where $\Omega \subseteq C^\omega$ a qualitative objective.

A configuration of such a timed automaton is a pair $(\ell, v)$ where $\ell \in \mathcal{L}$ and $v: \mathcal{C} \to \mathbb{R}_{\ge 0}$. The set of configurations is the set of vertices of the infinite-state game defined by $\mathcal{T}$.

The actions of both players are pairs $(d,e)$ where $d \in \mathbb{R}_{\ge 0}$ is a delay they want to wait before playing their controlled action $e$. Action $(d,e)$ is available for Eve (resp. Adam) in configuration $(\ell,v)$ if $e \in E_{Eve}(\ell)$ (resp. $e \in E_{Adam}(\ell)$) and, writing $e = (\ell,g,R,\ell')$, if additionally $v+d \models g$; in other terms, the clock constraint (called guard hereafter) on $e$ must hold true under the clock valuation reached after elapsing $d$ time units. We add an extra dummy action $\perp$ for the case where some player has no available action (this action is only available if no other actions are).

Once both players have selected an action available from configuration $(\ell, v)$, the
action $(d, e)$ with smallest delay is performed (by breaking ties in favor of Adam), leading to configuration $(\ell', (v+d)[R \leftarrow 0])$: this corresponds to letting $d$ time units elapse, thereby reaching configuration $(\ell, v+d)$, and to following edge $e$ (which by construction is available from $(\ell, v+d)$). We define step$((\ell, v), (d, e))$ for the configuration $(\ell', (v+d)[R \leftarrow 0])$ reached from $(\ell, v)$ by applying action $(d, e)$.

This definition captures the concurrent nature of the interaction between a controller (Eve) and its environment (Adam) in a real-time system, since none of the players knows in advance how long the opponent will want to wait before performing her transition. The semantics of a timed arena $(\mathcal{L}, \mathcal{C}, E_{\text{Eve}}, E_{\text{Adam}})$ can then formally be defined in terms of a concurrent arena (following the definition of Section 8.1). The underlying graph $(V, E)$ is such that $V = \mathcal{L} \times \mathbb{R}^{\ge 0}$, and $E = V \times C \times V$; the set of actions of Eve is $\mathbb{R}_{\ge 0} \times E_{\text{Eve}}$, and that of Adam is $\mathbb{R}_{\ge 0} \times E_{\text{Adam}}$; finally, the transition function, which is not stochastic in our case, maps any configuration $(\ell, v)$ and pair of actions $(d_{\text{Eve}}, e_{\text{Eve}})$ and $(d_{\text{Adam}}, e_{\text{Adam}})$ to the edge $((\ell, v), \gamma, \text{step}((\ell, v), (d, e)))$, where $(d, e) = (d_{\text{Eve}}, e_{\text{Eve}})$ and $\gamma = c(e_{\text{Eve}})$ if $d_{\text{Eve}} < d_{\text{Adam}}$, and $(d, a) = (d_{\text{Adam}}, e_{\text{Adam}})$ and $\gamma = c(e_{\text{Adam}})$ otherwise.

A path in a timed arena $\mathcal{T}$ then is a path in its associated infinite-state concurrent arena. The qualitative objective $\Omega$ can then be evaluated along runs of a timed arena in the natural way.

Contrary to Chapter 7, in this chapter we only consider deterministic strategies<fnref n="1" />. As a result, timed games are not determined, as illustrated in the following example.

<figure><img src="image_72.png" /><figcaption>Figure 9.2: Timed arena $\mathcal{A}_2$. Solid arrow is Eve's, dashed one is Adam's.</figcaption></figure>

**Example 2 (Timed Games are not determined).** In the timed arena $\mathcal{A}_2$ defined in Figure 9.2, from configuration $(\ell_0, \bar{0})$, Eve does not have a winning strategy to reach location $\ell_1$, but Adam does not have a winning strategy either to avoid $\ell_1$. In fact, available moves for both players consist in $(d, (\ell_0, \ell_1))$ with $0 < d < 1$ for Eve, and $(d', (\ell_0, \ell_2))$ with $0 < d' < 1$ for Adam. Thus, for any particular delay $0 < d < 1$ chosen by Eve, Adam has a possible delay $d < d' < 1$ which leads to $\ell_2$, which is losing for Eve. This shows that Eve does not have a winning strategy. The argument is however symmetric, and Adam also does not have a winning strategy to avoid $\ell_1$. Timed games are thus non determined.

**Example 3 (Winning strategy on running example).** Let us consider again the example of Figure 9.1 and see whether Eve has a winning strategy from the initial configuration. At the initial configuration $\ell_1, x = 0$, Eve needs to make a move towards $\ell_2$ while $x \le 1$ since whenever $x > 1$, Adam can move to $\ell_5$ which guarantees Eve's lost. Assume the game proceeds to $\ell_2$ with any value $x \le 1$. Here, Eve can try to wait until $x \ge 2$ and go to G. However, if $x < 1$, then Adam can move to $\ell_3$. From this location, Eve can guarantee to come back to $\ell_2$ with $x = 1$, and then move to G and win the game. Assume

<footnote n="1">¹Adding randomization over the infinite sets of actions is beyond the scope of this chapter.</footnote>
now that from $l_1$, the game proceeds to $l_3$ with $x = 0$ due to Adam's move. Again, Eve can wait for 1 time unit, and go back to $l_2$ with $x = 1$, and win the game. Hence, Eve has a winning strategy from $l_1$ for all $x \le 1$, and from $l_2$ for all values of $x$.

In this chapter, the main problem we are interested in is determining whether Eve has a strategy for her reachability objective. Let $\vec{0}$ denote the clock valuation assigning 0 to all clocks.

**Problem 9 (Solving a timed reachability game).**

**INPUT:** A timed arena $\mathcal{T}$, initial location $l_0$, and a reachability objective $\text{Reach}(\text{Win})$

**OUTPUT:** Does Eve has a winning strategy in $(\mathcal{T}, \text{Reach}(\text{Win}))$ from configuration $(l_0, \vec{0})$.

The difficulty of this problem is that the concurrent game $((V, E), \Delta, \Omega)$ has an infinite state-space, and players have infinitely many actions. We thus start by studying a data structure to represent sets of states and operations to compute successors and predecessors on these sets. We then give two algorithms to solve the above problem. We also show how such a strategy for Eve can be computed and finitely represented.

## 9.2 State-Space Representation

We introduce a data structure to represent sets of clock valuations and manipulate them efficiently in order to compute successors and predecessors in a given timed game. This will allow us to use a fixed point characterization of the winning states analogous to that in finite games as in Chapter 2.

A zone is any subset of $\mathbb{R}_{\ge 0}^2$ that can be defined using a clock constraint (hence a zone is convex). We will see that sets of states that appear when exploring the state space of a timed game can be represented using zones. We use the *difference-bound matrices* to represent zones: this is one of the main data structures used in timed-automata verification [Dil90, BM83]. The idea is to store, in a matrix, upper bounds on clocks and on differences of pairs of clocks. Formally, given a clock set $\mathcal{C} = \{x_1, \dots, x_m\}$, we define $\mathcal{C}_0 = \mathcal{C} \cup \{x_0\}$ where $x_0$ is seen as a special clock which is always 0. A *difference-bound matrix (DBM)* is a $|\mathcal{C}_0| \times |\mathcal{C}_0|$ matrix with coefficients in $\{\le, <\} \times \mathbb{Z}$. For any DBM $M$, the $(i, j)$-component of the matrix $M$ will be written $(<_{i,j}^M, M_{i,j})$ where $<_{i,j}^M$ is the inequality in $\{\le, <\}$, and $M_{i,j}$ the integer coefficient. A DBM $M$ defines the zone

$$[M] = \left\{ v \in \mathbb{R}_{\ge 0}^{\mathcal{C}} \mid \bigwedge_{0 \le i, j \le |\mathcal{C}_0|} v(x_i) - v(x_j) <_{i,j}^M M_{i,j} \right\},$$

where $v(x_0) = 0$.

**Example 4 (An example of a DBM).**

Consider the clock set $\mathcal{C} = \{x_1, x_2\}$ and the zone Z defined by $x_1 \le 1 \land x_1 - x_2 \le 0 \land x_2 \le 3 \land x_2 - x_1 \le 2$, which can be written as the following DBM: For instance, $M[2, 0] = (\le, 3)$ represents the constraint $x_2 - x_0 \le 3$, i.e., $x_2 \le 3$. The diagram to the right of the figure represents the set $[M]$.
<figure><img src="image_73.png" /><figcaption>Figure 9.3: Example of a DBM</figcaption></figure>

We now define elementary operations on DBMs which are used to explore the state space of timed games. We start by giving set-theoretic definitions and then comment on their computation with DBMs.

Let $Post_{\ge 0}(Z)$ denote the zone describing the *time-successeurs* of Z, and $Pre_{\ge 0}(Z)$ the *time-predecessors* of Z. Formally,

$$Post_{\ge 0}(Z) = \{v \in \mathbb{R}_{\ge 0}^{\mathcal{C}} \mid \exists t \ge 0. v - t \in Z\}$$

$$Pre_{\ge 0}(Z) = \{v \in \mathbb{R}_{\ge 0}^{\mathcal{C}} \mid \exists t \ge 0. v + t \in Z\}.$$

Given $R \subseteq \mathcal{C}$, we also define

$$Reset_R(Z) = \{v \in \mathbb{R}_{\ge 0}^{\mathcal{C}} \mid \exists v' \in Z. v = v'[R \leftarrow 0]\}$$

$$Unreset_R(Z) = \{v \in \mathbb{R}_{\ge 0}^{\mathcal{C}} \mid \exists v' \in Z. v' = v[R \leftarrow 0]\}.$$

These operations, together with intersection, suffice to describe one-step successors and predecessors by an edge of a timed automaton. For instance, given edge $e = (\ell, g, R, \ell')$ and set $S \subseteq \mathbb{R}_{\ge 0}^{\mathcal{C}}$, the set of states that are reached after letting time elapse and taking edge $e$ can be obtained as

$$Post_e(S) = Reset_R(Post_{\ge 0}(S) \cap G),$$

where $G$ denotes the zone corresponding to the guard $g$. Similarly, we can compute the predecessors of $S$ by edge $e$ as

$$Pre_e(S) = Pre_{\ge 0}(G \cap Unreset_R(S)).$$

We illustrate these constructions on Figure 9.4.

<figure><img src="image_74.png" /><figcaption>Figure 9.4: Operations on zones</figcaption></figure>

It is not hard to prove that the above operations preserve zones: if $S$ is a zone, then so is the result of any of these operations. Moreover, each single operation can be
computed in time $O(|C|^3)$ using the DBM representation. The underlying algorithms often modify some elements of the matrix and run an all-pairs shortest path algorithm, namely the Floyd-Roy-Warshall algorithm, on a graph whose adjacency matrix is the given DBM. Computing the shortest paths renders the DBM *canonical*; in fact, this allows one to compute the tightest constraints on all differences of clock pairs, and this can be shown to yield a unique representation of a given zone.

Let us call the above operations *basic operations* on DBMs [BY04].

**Theorem 101 (Complexity of basic operations on DBMs).** *Given a DBM of size $n \times n$, any basic operation yields a DBM and can be computed in time $O(n^3)$.*

Observe that a DBM always describes a convex subset of $\mathbb{R}^{c}_{\ge 0}$ since it is a con- junction of convex clock constraints. However, the set of winning states is in general non-convex in timed games. The simple arena of Figure 9.5 provides an example: if Eve's objective is to reach $\ell_1$, then it should just avoid the configurations satisfy- ing $1 \le x_1, x_2 \le 2$. But this set of predecessors is then non-convex as shown in Fig- ure 9.5. We thus have to work with unions of zones, also called federations of zones, or *federations* for short.

<figure><img src="image_75.png" /><figcaption>Figure 9.5: Winning configurations (in $\ell$) for Eve to ensure reaching $\ell_1$.</figcaption></figure>

One particular operation that we need is complementation. The complement of a convex set is of course not convex in general, but we can still compute, in polynomial time, the complement of a DBM $M$, written $M^c$, as a federation of DBMs.

**Theorem 102 (Complement of DBMs).** *The complement of a DBM of size $n \times n$ can be computed as a federation of at most $n(n-1)$ DBMs.*

The above theorem is seen easily as follows. Since a DBM represents a conjunction of constraints, the complement is computed easily as the disjunction of the complement of each elementary constraint appearing in it. For instance, the complement of $x_1 \le 1 \land x_2 \ge 2$ is $x_1 > 1 \lor x_2 < 2$, which can be represented as the federation of two zones.

In the rest of this chapter, we describe two algorithms to solve timed games using the DBM data structure and the operations introduced above. Our algorithms are ex- tensions of those used for finite games, but we explore the set of zones instead of the set of vertices, and predecessor and successor operations are replaced by their zone-based counterparts.

As for finite games, we are interested in computing a fixed point to determine whether a given configuration is winning for Eve. We start by introducing the zone- based counterparts of the controllable predecessors operator which is the main tool in the algorithms.
## 9.3 Controllable-Predecessor Operator

We present the controllable-predecessor operator which, given sets of states X and Y, returns the set of states from which Eve can reach X in one step, while avoiding states of Y during Eve's delay. Intuitively, the states in Y are the states from which Adam may force an action leading outside of X, which Eve would better avoid.

Recall that $V = \mathcal{L} \times \mathbb{R}_{\ge 0}^e$. The set of safe time-predecessors to reach $X \subseteq V$ while avoiding $Y \subseteq V$ is defined as follows:

$$ \mathrm{Pred}_{\ge 0}(X, Y) = \{ (\ell, v) \in V \mid \exists d \ge 0. (\ell, v+d) \in X \wedge \\ \qquad \forall d' \in [0, d). (\ell, v+d') \notin Y \}. $$

In words, from any configuration of $\mathrm{Pred}_{\ge 0}(X, Y)$, the set X can be reached by delaying while never crossing any configuration of Y on the way. For any $X \subseteq V$, let us denote

$$ \mathrm{Pred}_c(X) = \{ (\ell, v) \in V \mid \exists e \in E_{\mathrm{Eve}}(\ell). \exists (\ell', v') \in X. (\ell, v) \xrightarrow{e} (\ell', v') \}. $$

This is the set of immediate predecessors of X by edges in $E_{\mathrm{Eve}}$. Symmetrically, we define $\mathrm{Pred}_u(X)$ using $E_{\mathrm{Adam}}$ instead of $E_{\mathrm{Eve}}$. Our controllable-predecessor operator is then defined as

$$ \pi(X) = \mathrm{Pred}_{\ge 0}(X \cup \mathrm{Pred}_c(X), \mathrm{Pred}_u(V \setminus X)). $$

Intuitively, the states in $\pi(X)$ are those from which Eve can wait until she can take a controllable transition to reach X, and so that no transitions that Adam could take while Eve is waiting may lead outside of X.

**Lemma 126.** The operator $\pi$ is order-preserving: if $X \subseteq Y$, then $\pi(X) \subseteq \pi(Y)$.

**Example 5** (Example for the controllable predecessor operator). Consider the timed game to the left of Figure 9.6. In that game, Eve can reach her target when clock $x_2$ reaches value 3 while $x_1$ is in $[1; 4]$. However, Adam can take the game to a bad state when simultaneously $x_1 \in [1; 2]$ and $x_2 \le 2$. The diagram to the right of Figure 9.6 shows the set of winning valuations for Eve: it is computed as $\mathrm{Pred}_{\ge 0}(X, Y)$ where $X = \mathrm{Pred}_c(\{W\} \times \mathbb{R}_{\ge 0})$ and $Y = \mathrm{Pred}_u(\{\ell_0, \ell_1\} \times \mathbb{R}_{\ge 0})$.

<figure><img src="image_76.png" /><figcaption>Figure 9.6: Controllable predecessors</figcaption></figure>

**Remark 12** (Reduction for zero-sum objectives). When considering zero-sum objectives (which we do in this chapter), a turn-based arena can be built to decide whether
Eve has a winning strategy (and possibly construct one). Intuitively, the turn-based arena is obtained by letting Eve first pick a pair $(d, e)$ with $e \in E_{Eve}$, and then letting Adam either respect this choice (i.e., play a larger delay) or preempt Eve's action by choosing $(d', e')$ with $d' \le d$ and $e' \in E_{Adam}$. Eve has a winning strategy in this turn-based arena if, and only if she has one in the original game. However, this does not apply to Adam; if he has a winning strategy, this only means that Eve does not have a winning strategy in the original game.

Given $\mathcal{T} = (\mathcal{L}, \mathcal{C}, E_{Eve}, E_{Adam}, c)$, we define the arena $\mathcal{A} = (V, V_{Eve}, V_{Adam}, E, c'')$ with objective $\Omega$, where $V_{Eve} = \mathcal{L} \times \mathbb{R}_{\ge 0}^{\mathcal{C}}$ and $V_{Adam} = \mathcal{L} \times \mathbb{R}_{\ge 0}^{\mathcal{C}} \times (\mathbb{R}_{\ge 0} \times E_{Eve} \cup \{\perp\})$. The set of successors of configuration $(\ell, v) \in V_{Eve}$ is the set $\{(\ell, v, a) \mid a \text{ available at } (\ell, v)\}$. From a configuration $((\ell, v), (d, e)) \in V_{Adam}$, several cases may occur:

* if Adam has no available action from $(\ell, v)$, or if he can only play actions $(d', e')$ with $d' > d$, then the only transition from $((\ell, v), (d, e))$ goes to step $((\ell, v), (d, e))$;

* Otherwise, for all actions $(d', e')$ for Adam satisfying $d' \le d$, there is a transition from $((\ell, v), (d, e))$ to step $((\ell, v), (d', e'))$. Moreover, if Adam has an available action $(d', e')$ with $d' \ge d$, then there is also a transition from $((\ell, v), (d, e))$ to step $((\ell, v), (d, e))$.

From a configuration $((\ell, v), \perp)$, there is a transition to step $((\ell, v), (d', e'))$ for each available action $(d', e')$ of Adam. The coloring function is defined as $c''((\ell, v)) = c(\ell)$ and $c''((\ell, v), (d, e)) = c(\ell)$.

## 9.4 Backward Algorithm

Given the DBM data structure we presented, a backward fixed point algorithm follows for computing the winning configurations in a timed game:

**Theorem 103 (Correctness of the backward algorithm).** For any timed game $\mathcal{A}$ and target set $G \subseteq V_{Eve}$, the limit $\lim_{k \to \infty} \pi^k(G)$ exists, and is reached in a finite number of steps. This limit is precisely the set of states from which the controller has a winning strategy for reaching $G$.

*Sketch.* We briefly explain why the fixed point computation terminates and refer to [AMPS98, CDF+05] for more details. The proof relies on the notion of *regions*. Intuitively, regions are minimal zones, not containing any other zone. More precisely, writing $K$ for the maximal (absolute) integer constant appearing in the timed game, the set of regions is the set of zones associated with DBMs $(\prec_{i,j}, M_{i,j})$ such that

* $M_{i,j} \in [-K; K] \cup \{-\infty; +\infty\}$ for all $i$ and $j$;

* for all $i \neq j$,

- either $M_{i,j} = -M_{j,i}$ and $\prec_{i,j} = \prec_{j,i} = \le$,

- or $|M_{i,j} + M_{j,i}| = 1$ and $\prec_{i,j} = \prec_{j,i} = <$,

- or $(\prec_{i,j}, M_{i,j}) = (<, +\infty)$ and $(\prec_{j,i}, M_{j,i}) = (<, -K)$.
The set of regions form a finite partition of $\mathbb{R}^{\mathcal{G}}$. The main argument for the proof is that the image by $\pi$ of any finite union of regions is a finite union of regions. Since $\pi$ is non-decreasing, the sequence $\pi^k(G)$ converges after finitely many steps.

The fact that $\pi^k(G)$ may only contain winning configurations follows from our construction, and can be proved easily by induction on $k$. One can also show that for all configurations outside of $\pi^k(G)$, there is no strategy that is winning within $k$ steps. This follows since the definition of $\pi(\cdot)$ gives the actions to be played by Adam to prevent Eve from winning. Note that this does not necessarily yield a winning strategy for Adam, since the game is not determined. $\square$

## 9.5 Forward Algorithm

The backward algorithm we just presented is conceptually simple, but it is often not very efficient in practice, as federations tend to grow too much in size in each iteration of the computation. The forward algorithm we will now present is more efficient in practice. It performs a forward exploration and only applies the controllable predecessor along branches that actually reach the target state from the initial state. If the witness trace is not excessively long, which is often the case in practice, this limits the size of the federations.

We present below the algorithm proposed in [CDF+05], and as a first step, we explain the untimed version of that algorithm, based on an algorithm of Liu and Smolka for computing fixed points [LS98].

### A Forward Algorithm for Finite-State Games

The original algorithm of Liu and Smolka is expressed in terms of *pre-fixed points* in *dependency graphs*: a dependency graph is a pair $G = (V, E)$ in which $E \subseteq V \times 2^V$ relates states with sets of states. For any order-preserving function $f: 2^V \to 2^V$ (*order-preserving* meaning non-decreasing for the $\subseteq$-relation), a *pre-fixed point* is a set $X \subseteq V$ for which $f(X) \subseteq X$; it is a *fixed point* if $f(X) = X$. By Knaster-Tarski theorem, such functions always admit a least pre-fixed point which is also the least fixed point.

Fix a dependency graph $G = (V, E)$. For $W \subseteq V$, we define a mapping $f_W: 2^V \to 2^V$: for each $X \subseteq V$, we let $f_W(X) = W \cup \{v \in V \mid \exists (v, Y) \in E. Y \subseteq X\}$. Clearly, $X \subseteq X'$ implies $f_W(X) \subseteq f_W(X')$, so that $f_W$ admits a least (pre-)fixed point. The Liu-Smolka algorithm aims at deciding whether a given vertex $v_0 \in V$ belongs to the least fixed point of $f_W$. Classical algorithms for computing least fixed points consist in iteratively computing $(f_W^i(\emptyset))_i$ until convergence (assuming $V$ is finite). Observe that this corresponds to the algorithm of Theorem 103 for timed games. The Liu-Smolka algorithm proceeds from $v_0$, and explores the dependency graph until it can claim that $v_0$ is, or that it is not, in the least fixed point of $f_W$.

Before tackling the algorithm, let us link least fixed points in dependency graphs and winning sets in concurrent games (with reachability objectives): with a concurrent arena $\mathcal{C} = (V, \text{Act}, \delta, c')$ and a target set Win, we associate the dependency graph $G = (V, E)$, where $(v, T) \in E$ whenever $v \in V$ and $T \subseteq V$ is such that there exists an action $a$ for which $T = \{v' \mid \exists a' \in \text{Act}. v' = \delta(v, a, a')\}$. Then for any set $X \subseteq V$, the set $f_{\text{Win}}(X)$
contains Win and all the states from which Eve can force a visit to X in one step.
We then have:

**Proposition 3.** *The least fixed point of $f_{Win}$ in G corresponds to the set W of winning states for Eve in $\mathscr{C}$.*

*Proof.* The winning states of Eve form a pre-fixed point of $f_{Win}$ containing Win: indeed, for any $v \in f_{Win}(W)$, either $v \in$ Win, or Eve has an action to move from $v$ to some state in $W$. Hence $v$ is winning, i.e., $v \in W$.

Conversely, from any state $v$ that is not in the least pre-fixed point $X$, for any edge $(v, T)$, there is a state $v' \in T$ that again is not in $X$. This defines a strategy for Adam to avoid reaching Win, so that Eve does not have a winning strategy from $v$. $\square$

<caption>**Algorithm 9.1:** Liu-Smolka algorithm for least fixed point of $f_W$</caption>

**Data:** A dependency graph $G = (V, E)$, a set $W \subseteq V$, a node $v_0 \in V$
**Result:** Is $v_0$ in the least fixed point of $f_W$?
**for** $v \in V$ **do**
| **if** $v \in W$ **then** $F(v) := 1$;
| **else if** $v == v_0$ **then** $F(v) := 0$;
| **else** $F(v) := \perp$;
**Dep**($v_0$) := $\emptyset$;
**Wait** := $\{(v, T) \in E \mid v = v_0\}$;
**while** (Wait $\neq$ $\emptyset$ and $F(v_0) == 0$) **do**
| $(v, T) := \text{pop}(\text{Wait})$; // case 1
| **if** $F(v) == 0$ and $\forall v' \in T. F(v') == 1$ **then**
| & $F(v) := 1$; // case 2
| & **Wait** := Wait $\cup$ Dep($v$);
| **else if** $\exists v' \in T. F(v') == 0$ **then**
| & $\text{Dep}(v') := \text{Dep}(v') \cup \{(v, T)\}$;
| **else if** $\exists v' \in T. F(v') == \perp$ **then**
| & $F(v') := 0$;
| & $\text{Dep}(v') := \{(v, T)\}$;
| & **Wait** := Wait $\cup \{(w, U) \in E \mid w = v'\}$;
**return** $F(v_0)$ // case 3

Algorithm 9.1 can be seen as an alternation of forward exploration and backward propagation. Intuitively, the algorithm first explores the graph in a forward manner, remembering for each node $v$ the set $\text{Dep}(v)$ of nodes that *depend* on $v$, and have to be reexplored if the status of $v$ is updated. For each $v$, the algorithm maintains a value $F(v)$, which is $\perp$ if $v$ has not been explored yet, 0 if $v$ has been explored but not

<footnote n="2">²Our version of the algorithm slightly differs from the original one [LS98]: we let $\text{Dep}(v') := \{(v, T)\}$ at the penultimate line of the **while** loop (which otherwise results in a wrong result, as already noticed in [JLSØ13]), reinforce the condition for case 1 (which otherwise would not guarantee termination), and reinforce the condition of the **while** loop to get earlier termination.</footnote>
yet been shown to be winning, and 1 if $v$ is known to be winning. Whenever a vertex $v$ whose all successors are winning is found, the value of $v$ is set to 1, and its parents (in $\text{Dep}(v)$) are scheduled to be visited again to check whether their statuses have to be changed. This is how the backward propagation is triggered; in fact, the search will climb in the tree as long as the values of vertices can be updated to 1.

The correctness of this algorithm relies on the following lemma [LS98]:

**Lemma 127 (Invariant).** *The following properties hold at the end of each run in the while loop of Algorithm 9.1:*

• for any $v \in V$, if $F(v) = 1$, then $v$ belongs to the least fixed point containing $W$;

• for any $v \in V$ with $F(v) = 0$, and any $(v, T) \in E$, either $(v, T) \in \text{Wait}$ or $(v, T) \in \text{Dep}(v')$ for some $v' \in T$ with $F(v') = 0$.

*Proof.* We fix an execution of Algorithm 9.1, and prove that both claims are true at the beginning and end of each iteration through the **while** loop. To clarify the presentation, we use superscript *i* to indicate the value of variables at the end of the *i*-th run through the loop, so that Wait³ is the value of variable Wait after three iterations (and Wait⁰ is its value after initialization). In particular, $(v^i, T^i)$ is the symbolic transition popped from the Wait list during the *i*-th iteration (and is not defined for *i* = 0).

Let us first prove the first property: the initialization phase clearly enforces that if $F^0(x) = 1$, then $x \in W$, which is included in any fixed point of $f_W$. Now, assume that the property holds true at the beginning of the *i*-th run through the loop (i.e., if $F^{i-1}(x) = 1$, then *x* is in the least fixed point), and pick some $x \in V$ such that $F^i(x) = 1$. If $F^{i-1}(x) = 1$, our result follows; if not, then the *i*-th iteration of the loop must have run via case 1, hence $F^{i-1}(x') = 1$ for all $x' \in T^i$. By our induction hypothesis, this indicates that $T^i$ is part of the least fixed point, and by definition of $f_W$, *x* must also belong to the least fixed point.

The second statement also clearly holds after initialization: initially, $F^0(x) = 0$ only for $x = v_0$, and all transitions from $v_0$ have been stored in Wait⁰. We now assume that the property holds when entering the **while** loop for the *i*-th time, and consider *x* such that $F^i(x) = 0$ at the end of that loop. We pick $(x, Y) \in E$.

• if the *i*-th run through the loop visits case 1, then already $F^{i-1}(x) = 0$ (hence $x \neq v^i$). Then either $(x, Y) \in \text{Wait}^{i-1}$, or $(x, Y) \in \text{Dep}^{i-1}(x')$ for some $x' \in Y$ with $F(x') = 0$. In the former case: since $x \neq v^i$, if $(x, Y) \in \text{Wait}^{i-1}$ then also $(x, Y) \in \text{Wait}^i$; in the latter case: if $(x, Y) \in \text{Dep}^{i-1}(x')$ for some $x' \in Y$ with $F(x') = 0$, then (i) either $x' = v^i$, and $(x, Y) \in \text{Wait}^i$ because $\text{Dep}^{i-1}(v^i) \subseteq \text{Wait}^i$ (last line of case 1), (ii) or $x' \neq v^i$, and $(x, Y) \in \text{Dep}^{i-1}(x') = \text{Dep}^i(x')$ and $F^i(x') = F^{i-1}(x') = 0$.

• if the *i*-th run goes to case 2, then again $F^{i-1}(x) = 0$, and the induction hypothesis applies: either $(x, Y)$ is in $\text{Wait}^{i-1}$, or it is in $\text{Dep}^{i-1}(x')$ for some $x' \in Y$ with $F^{i-1}(x') = 0$. For the latter case, observe that $\text{Dep}^{i-1}(x') \subseteq \text{Dep}^i(x')$, and $F^i(x') = F^{i-1}(x')$ when running case 2; for the former case, we have $\text{Wait}^i = \text{Wait}^{i-1} \setminus \{(v^i, T^i)\}$, so that $(x, Y)$ remain in $\text{Wait}^i$ if $(x, Y) \neq (v^i, T^i)$; finally, if $(x, Y) = (v^i, T^i)$, then case 2 precisely adds $(v^i, T^i)$ to $\text{Dep}^i(v')$ for some $v' \in T^i$ with $F^i(v') = 0$, which concludes the proof for this case.
* for case 3, we first consider the case where $x$ is the state $v'$ selected at the beginning of case 3: in that case, all transitions from $x$ are added to Wait, so that $(x, Y) \in \text{Wait}^i$. Now, if $x$ is not the selected state $v'$, then $F^{i-1}(x) = 0$, and again either $x \in \text{Wait}^{i-1}$ or $x \in \text{Dep}^{i-1}(x')$ for some $x' \in Y$ with $F^{i-1}(x') = 0$. The latter case is preserved when running case 3; if $x \in \text{Wait}^{i-1}$: if $(x, Y) \neq (v^i, T^i)$, then $x \in \text{Wait}^i$, while if $(x, Y) = (v^i, T^i)$, then $(x, Y) \in \text{Dep}^i(v')$ for the state $v' \in T^i$ selected at the beginning of case 3 (and for which $F^i(v') = 0$).

□

As a corollary, if the algorithm terminates after $n$ rounds of the **while** loop, then either $F^n(v_0) = 1$, or $F^n(v_0) = 0$ and Wait$^n = \emptyset$.

* From the first claim of the lemma above, the former case entails that $v_0$ belongs to the least fixed point.

* Now consider the second case, and let $B = \{v \in V \mid F^n(v) \in \{\perp, 1\}\}$. We prove that $f_W(B) \subseteq B$. For this, we pick $v \in f_W(B)$:

- if $v \in W$, then $F(v)$ is set to 1 initially, and may never be changed, so that $v \in B$;

- otherwise, there is a transition $(v, T)$ such that $T \subseteq B$. If $v \notin B$, then $(v, T) \in \text{Dep}^n(v')$ for some $v' \in T$ with $F^n(v') = 0$, which contradicts the fact that $T \subseteq B$.

This proves that $f_W(B) \subseteq B$, so that $B$ is a pre-fixed point of $f_W$. It thus contains the least (pre-)fixed point of $f_W$, so that any state $v$ not in $B$ (i.e., with $F^n(v) = 0$) for sure does not belong to that least fixed point. In particular, $v_0$ is not in the fixed point.

It remains to prove termination. For this, we first notice that, for any hyper-edge $(v, S)$, if $(v, S) \in \text{Dep}^i(v')$ then $(v, S) \in \text{Wait}^j$ for some $j < i$, and if $(v, S) \in \text{Wait}^j$ or $(v, S) \in \text{Dep}^j(v')$ for some $v'$, then $F^j(v) \neq \perp$.

We then set

$$M = 2|\text{Wait}| + 2 \sum_{v \text{ s.t. } F(v)=\perp} |\{(v, S) \in E\}| + \sum_{v \text{ s.t. } F(v)=0} |\text{Dep}(v)| - \sum_{v \text{ s.t. } F(v)=1} |\text{Dep}(v)|$$

again writing $M^i$ for the value of $M$ after the $i$-th run through the **while** loop. This value is at most $2|E|$ when entering the **while** loop for the first time; clearly, it can never go below $-|E|$. We now prove that $M^i < M^{i-1}$, which implies termination of the algorithm.

Consider the $i$-th run through the loop, popping $(v^i, T^i)$ from Wait$^{i-1}$ (which decreases $M$ by 2). We consider all three cases:

* if case 1 applies, $F^i(v)$ is set to 1. The set $\text{Dep}^{i-1}(v)$ is added to Wait$^i$. This globally leaves $M$ unchanged, so that globally $M^i = M^{i-1} - 2$;
* if case 2 applies, $\text{Dep}^{i-1}(v')$ is augmented by (at most) one edge, and since $F^i(v') = 0$, this increases $M$ by at most 1. Hence globally $M^i \le M^{i-1} - 1$;

* finally, case 3 increases $M$ by 1: the edges added to Wait are compensated by the fact that $F(v')$ no longer is $\perp$, and only one extra edge has to be considered in the second sum. Hence again $M^i \le M^{i-1} - 1$.

This concludes the correctness proof of Algorithm 9.1.

**Theorem 104.** *Algorithm 9.1 terminates, and returns 1 if, and only if, $v_0$ belongs to the least fixed point of $fw$.*

Using Proposition 3, we get a *forward* algorithm for deciding if a given state of a concurrent game is winning for Eve. This corresponds to the OTFUR algorithm of [CDF+05].

## Extension to Timed Games

We now explain how to adapt the algorithm above to (infinite-state) timed games. For efficiency, the algorithm relies on zones (and DBMs); instead of computing whether a given zone $(\ell, Z)$ is winning, the algorithm maintains, for each zone $S = (\ell, Z)$ it explores, a subzone $(\ell, Z')$ of configurations that it knows are winning; this subzone is stored as $F(S)$, and is updated during the execution. As in Algorithm 9.1, a waiting list keeps track of the zones to be explored, and a dependency list stores the list of nodes to be revisited upon update of the winning subzone of a zone. The algorithm is given in Algorithm 9.2.

The correctness of the algorithm can be proven using the following lemma. We omit the proof of this lemma, as it is tedious and does not contain any difficult argument.

**Lemma 128.** *The following properties hold at the end of each run through the while loop of Algorithm 9.2:*

* for any $S \in \text{Passed}$ and any transition $\alpha$, if $T = \text{Post}_{\ge 0}(\text{Post}_{\alpha}(S)) \neq \emptyset$, then either $(S, \alpha, T) \in \text{Wait}$, or $T \in \text{Passed}$ and $(S, \alpha, T) \in \text{Dep}(T)$;

* for any $S \in \text{Passed}$ and $q \in F(S)$, $q$ is winning for Eve;

* for any $S \in \text{Passed}$ and $q \in S \setminus F(S)$, either Wait contains a symbolic transition $(S, \alpha, S')$ from $S$ with $S' \in \text{Passed}$, or

$$ q \notin \text{Pred}_{\ge 0} \left( F(S) \cup \bigcup_{\substack{S \xrightarrow{c} V \\ V \in \text{Passed}}} \text{Pred}_c(F(V)), \quad \bigcup_{\substack{S \xrightarrow{u} V \\ V \in \text{Passed}}} \text{Pred}_u(V \setminus F(V)) \right) \cap S. $$

The proof is omitted but can be found in [CDF+05].

Using these invariants, we get the following result:

**Lemma 129.** *If Algorithm 9.2 terminates, all configurations in $F(S)$ for any $S \in \text{Passed}$ are winning for Eve; if additionally $\text{Wait} = \emptyset$, then all configurations in $S \setminus F(S)$, for any $S \in \text{Passed}$, are losing for Eve.*
**Algorithm 9.2:** Symbolic on-the-fly algorithm for timed reachability

**Data:** A reachability timed game $\mathcal{G} = (\mathcal{A}, \text{Reach}(\text{Win}))$, a location $\ell_0 \in \mathcal{L}$

**Result:** Is $(\ell_0, \mathbf{0})$ winning for Eve?

$S_0 := \text{Post}_{\ge 0}(\ell_0, \mathbf{0});$

if $c(S_0) == \text{Win}$ then $F(S_0) := S_0$ else $F(S_0) := \emptyset$;

$\text{Passed} := \{S_0\};$ // Passed stores all configurations for which $F$ is defined

$\text{Dep}(S_0) := \emptyset$;

$\text{Wait} := \{(S_0, \alpha, T) \mid T = \text{Post}_{\ge 0}(\text{Post}_{\alpha}(S_0)) \neq \emptyset, \alpha \text{ transition of } \mathcal{G}\}$;

while ($\text{Wait} \neq \emptyset$ and $(v_0, \mathbf{0}) \notin F(S_0)$) do

(S, α, T)) := pop (Wait); // case A

if T ∈ Passed then
    Dep(T) := Dep(T) ∪ {(S, α, T)};
    W :=
        Pred$_{≥ 0}$ (F(S) ∪ ⋃$_{S \stackrel{c}{→} V}$ Pred$_c$(F(V)), ⋃$_{S \stackrel{u}{→} V}$ Pred$_u$(V \ F(V))) ∩
        S;
    if F(S) ⊊ W then
        F(S) := W;
        Wait := Wait ∪ Dep(S);
    else
        Passed := Passed ∪ {T}; // case B
        if c(T) == Win then
            F(T) := T;
            Wait := Wait ∪ {(S, α, T)}
        else
            F(T) := ∅;
            Dep(T) := {(S, α, T)};
            Wait := Wait ∪ {(T, α, U) | U = Post$_{≥ 0}$(Post$_{α}$(T)) ≠
                ∅, α transition of };

if $(v_0, \mathbf{0}) \in F(S_0)$ then return 1 else return 0;
Proof. The first statement corresponds to the second statement of Lemma 128. Now, assume Wait<sup>n</sup> = ∅ after termination at the n-th step, and let L = {q ∈ L × ℝ<sup>ℝ<sup>≥0</sup></sup> | ∃S ∈ Passed<sup>n</sup>. q ∈ S \ F<sup>n</sup>(S)}, and M be the complement of L. For any S ∈ Passed<sup>n</sup>, we then have M ∩ S ⊆ F<sup>n</sup>(S).

Pick $q \in \pi(M) \cup \text{Win}$, where we abusively write $\text{Win}$ to denote all configurations with location colored $\text{Win}$. We prove that $q \in M$:

* if $q \in \text{Win}$: assume $q \in L$, and pick $S \in \text{Passed}^n$ such that $q \in S \setminus F^n(S)$. Since $q \in S$, it holds $c(S) = \text{Win}$; but then $F^n(S)$ is defined (since $S \in \text{Passed}^n$), and it equals $S$ by initialization of $F$. This contradicts the fact that $q \in S \setminus F^n(S)$, hence $q \in M$.

* if $q \in \pi(M)$: we again assume $q \in L$. Then for some $S \in \text{Passed}^n$, $q \in S \setminus F^n(S)$. By the third property of Lemma 128, $q \notin W^n$ (because Wait<sup>n</sup> is empty). Since $M \cap U \subseteq F^n(U)$ for all $U \in \text{Passed}^n$ and $F^n(U) = \emptyset$ for all $U \notin \text{Passed}^n$, and by monotonicity, we get

$$q \notin \text{Pred}_{\ge 0} \left( (M \cap S) \cup \bigcup_{S \xrightarrow{c} V} \text{Pred}_c(M \cap V), \bigcup_{S \xrightarrow{u} V} \text{Pred}_u(V \setminus (M \cap V)) \right) \cap S.$$

Now, notice that any $S \in \text{Passed}^n$ is closed under $\text{Post}_{\ge 0}$. Then

$$\begin{aligned} \pi(M) \cap S &= \text{Pred}_{\ge 0}(M \cup \text{Pred}_c(M), \text{Pred}_u(\bar{M})) \\ &= \text{Pred}_{\ge 0}((M \cap S) \cup (\text{Pred}_c(M) \cap S), \text{Pred}_u(\bar{M})). \end{aligned}$$

Now, it can be checked that $\text{Pred}_c(M) \cap S \subseteq \bigcup_{S \xrightarrow{c} V} \text{Pred}_c(M \cap V)$ and $\text{Pred}_u(\bar{M}) \supseteq \bigcup_{S \xrightarrow{u} V} \text{Pred}_u(V \setminus (M \cap V))$. So the fact that $q \in \pi(M)$ and $q \in S$ leads to a contradiction. This entails that $q \notin L$, hence $q \in M$.

In the end, we have proven that $\pi(M) \cup \text{Win} \subseteq M$, so that $M$ is a pre-fixed point of $X \mapsto \pi(X) \cup \text{Win}$, hence it contains all winning configurations of Eve and $L$ only contains losing configurations. □

The procedure given in Algorithm 9.2 will in general not terminate: as in the case of timed automata, the number of zones generated by the algorithm may be infinite. This is classically avoided using *extrapolation*: this consists in abstracting the zones being considered by larger zones, defined by only using integer constants less than the maximal constant appearing in the timed arena (as we did for regions in the proof of Theorem 103). This can be proven to preserve correctness, and makes the number of zones finite. Termination follows by noticing that any triple $(S, \alpha, T)$ may be added to Wait only a finite number of times (bounded by the number of regions in $T$). We can then conclude:

**Theorem 105.** *Algorithm 9.2 terminates when extrapolation is used, and returns 1 if, and only if, $(\ell_0, \mathbf{0})$ is winning for Eve.*
Bibliographic references

Timed games were first introduced by Asarin, Maler, Pnueli and Sifakis [MPS95, AMPS98], in a slightly different form. Our presentation is based on the algorithms proposed by Liu and Smolka [LS98], and extended to timed games by Cassez, David, Fleury, Larsen and Lime [CDF+05]; its main advantage is that it runs on-the-fly, building (part of) the arena while exploring it, and terminating as soon as a winning strategy is found. A first on-the-fly algorithm was proposed by Tripakis and Altisen in [TA99], but it was not fully on-the-fly as it would run on a quotient graph of the timed arena, which involves an expensive preprocessing step.

Timed games—and already timed automata—may exhibit unrealistic behaviours, such as finite-duration executions containing infinitely many transitions (often referred to as *Zeno* behaviours). In our semantics, Adam may always prevent Eve from playing her move by choosing a shorter delay than hers, even if it means selecting a convergent sequence of delays. Figure 9.7 displays a simple example of such a situation: in that game, Adam may prevent Eve from reaching her winning state $q_1$ by always selecting a delay shorter than the delay proposed by Eve.

<figure><img src="image_77.png" /><figcaption>Figure 9.7: A timed game where Adam may prevent Eve from reaching $q_1$</figcaption></figure>

An alternative semantics of timed games was proposed by de Alfaro, Faella, Henzinger, Majumdar, and Stoelinga [dAFH+03] to circumvent this problem: it consists in blaming at each round the player playing the shortest delay, and declaring any player losing (even if she reaches her goal) in case the infinite sequence of delays converges and that player received infinitely many blames. For such a semantics, Eve has a winning strategy in the game of Figure 9.7, which consists in proposing a converging sequence of delays, until her action is applied; such a strategy requires infinite memory, but strategies with randomized delays can circumvent this [CHP08]. Other approaches to avoid arbitrary-precision strategies have been explored in [BMS15, BFM15, LLTW14, ORS14].

Timed games have been extended with weights, in order to model other quantities besides time (e.g. energy consumption). This is somewhat similar to the finite-state games extended with payoffs of Chapter 4; in the timed setting however, besides evolving along transitions in the game, the payoff is also modified when timed elapses, and the change is proportional to the time spent. As proven in [BBR05, BBM06], optimal reachability (a.k.a. the shortest-path problem) is undecidable in that setting, but arbitrary-precise approximation of the optimal cost can be computed [BJM15].

Timed games with partial observability have been investigated in [BDMP03]: in that setting, Eve only has partial observation of the state and clock valuation of the arena; she also owns a finite set of clocks she can use to measure other delays. Whether Eve has a winning strategy in such a setting has been proved decidable if the set of clocks
and their precision are fixed; it is undecidable if they are not fixed. A different setting was developed in [CDL$^+07]$, with *stuttering-invariant strategies*, which are triggered by observation changes. The on-the-fly algorithm presented in this chapter can be adapted to that setting [CDL$^+07].

The algorithm we presented in this chapter is implemented in the tool Uppaal TiGa [BCD$^+07]. Uppaal TiGa has been applied on various cases [CJL$^+09], and combined with reinforcement-learning techniques to efficiently synthesise, optimise and evaluate strategies for stochastic timed games [DJL$^+15]. Another approach, relying on abstraction-refinement techniques, was proposed in [EMP10]; it merges locations so as to obtain simpler games, while weakening one player and strengthening her opponent. Solving the smaller games provides approximations on the winning set, which are used to refine the abstractions and accelerate their analyses. This approach is implemented in the tool Synthia [PEM11].
PUSHDOOM GAMES

<figure><img src="image_78.png" /></figure>

<figure><img src="image_79.png" /></figure>
Chapter 10

# Pushdown Games

ARNAUD CARAYOL, OLIVIER SERRE

This chapter studies two-player games whose arena is defined by a pushdown system<fnref n="1" />. The vertices of the arena are the configurations of the pushdown system (i.e., pairs composed of a control state and a word representing the content of the stack) and the edges of the arena are defined by the pushdown system’s transitions. For simplicity, both the ownership of a configuration and the objective will only depend on the control state of the configuration. Hence the partition of all the configurations between the two players will simply be given by a partition the control states. We will mainly consider the parity objective. Via a standard reduction (using a deterministic parity automaton, see Section 1.4), parity pushdown game can be used to solve any pushdown game with an $\omega$-regular objectives (which in our setting is simply an $\omega$-regular set of infinite words over the alphabet of control states).

The main conceptual novelty of this chapter is that the arena is no longer finite. However as these games are described by a finite amount of information: the pushdown system, the ownership partition and the $\omega$-regular objective, they are amenable to algorithmic treatment. The first natural problem in this line is to decide the winner of the game from a given configuration. We will also consider the computation of *finite representations* for the winning regions and the winning strategies.

## 10.1 Notations

A pushdown system is a tuple $\mathcal{P} = (Q, \mathcal{Q}_{Eve}, \mathcal{Q}_{Adam}, \Gamma, \Delta, C)$ where:

* $Q$ is a finite set of control states with $Q = \mathcal{Q}_{Eve} \cup \mathcal{Q}_{Adam}$ which is partitioned between the two players Eve and Adam. Moreover with each state $q$ is associated a colour $c(q) \in C$;

<footnote n="1">¹We use here the term pushdown system rather than pushdown automaton to stress the fact that we are not considering these devices as language acceptors but rather focus on the transitions systems they define.</footnote>
• $\Gamma$ is the stack alphabet. There is a special bottom-of-stack symbol, denoted $\perp$, which does not belong to $\Gamma$; we let $\Gamma_{\perp}$ denote the alphabet $\Gamma \cup \{\perp\}$;

• $\Delta: Q \times \Gamma_{\perp} \to 2^{Q \times \{\text{pop, push}(\gamma) | \gamma \in \Gamma\}}$ is the transition relation. We additionally require that for all states $p, q \in Q$, $(q, \text{pop}) \notin \Delta(p, \perp)$, i.e., the bottom of stack symbol is never popped.

We call a pair $(p, s) \in Q \times \perp \Gamma^*$ a configuration of $\mathcal{P}$: $p$ is the control state of the configuration while $s$ is its stack content. We let $\text{sh}((p, s)) = |s| - 1$ denote the stack height of the configuration $(p, s)$. Intuitively, if $(q, \text{push}(\gamma))$ belongs to $\Delta(p, \gamma)$, the pushdown system in any configuration of the form $(p, s\gamma)$ can go to state $q$ after pushing the symbol $\gamma$ on top of the stack, leading to the configuration $(q, s\gamma\gamma')$. Similarly, if $(q, \text{pop})$ belongs to $\Delta(p, \gamma)$, the pushdown system in any configuration of the form $(p, s\gamma)$ can go to the configuration $(q, s)$ after poping the top symbol from the stack.

A pushdown system induces an arena $\mathcal{A} = (G, V_{\text{Eve}}, V_{\text{Adam}})$ called a pushdown arena where

• the set of vertices is the set $V = Q \times \perp \Gamma^*$ of configurations of $\mathcal{P}$ with $V_{\text{Eve}} = Q_{\text{Eve}} \times \perp \Gamma^*$ and $V_{\text{Adam}} = Q_{\text{Adam}} \times \perp \Gamma^*$;

• the set $E$ of edges induced by $\Delta$ is

$$E = \{((p, s\gamma), c(p), (q, s)) \mid (q, \text{pop}) \in \Delta(p, \gamma) \} \cup \{((p, s\gamma), c(p), (q, s\gamma\gamma')) \mid (q, \text{push}(\gamma')) \in \Delta(p, \gamma)\}.$$

**Remark 13.** In this chapter, we deviate slightly from the general setting used in the book as we colour vertices and not edges. Because we only consider qualitative objectives, it is more convenient to consider the equivalent setting where we label vertices by colours rather than edges which is the usual convention in pushdown games. In the definition of a pushdown arena, the colour of an edge is uniquely determined by the colour of the control state of the source vertex. Therefore, we also view in this chapter plays as sequences of vertices rather than sequences of edges.

Finally, a pushdown game is a game played on a pushdown arena. In this chapter we only consider qualitative objectives of the form $\Omega \subseteq C^\omega$ where $C$ is the set of colours. As in our definition, colours are associated to control states, the objective we consider only depend on the sequence of control states of the configurations visited along a play. By a slight abuse of notation, for a play $\pi \in V^*$, we let $\pi = (p_1, s_1)(p_2, s_2)\cdots \in \Omega$ denotes the fact that the sequences of colours $(c(p_i))_{i \ge 1}$ belongs to $\Omega$.

**Example 6.** Consider the pushdown system $\mathcal{P} = (Q, Q_{\text{Eve}}, Q_{\text{Adam}}, \Gamma, \Delta)$ where:

• $Q_{\text{Eve}} = \{q, r\}$ and $Q_{\text{Adam}} = \{p\}$; $c(p) = 1$, $c(q) = 2$ and $c(r) = 0$.

• $\Gamma = \{\gamma\}$ is a singleton.

• $\Delta(p, \perp) = \{(p, \text{push}(\gamma))\}$, $\Delta(p, \gamma) = \{(p, \text{push}(\gamma)), (q, \text{pop})\}$, $\Delta(q, \perp) = \{(r, \text{push}(\gamma))\}$, $\Delta(q, \gamma) = \{(q, \text{pop})\}$ and $\Delta(r, \gamma) = \{(q, \text{pop})\}$.
Figure 10.1 depicts the part of the pushdown arena $\mathcal{A}$ induced by $\mathcal{P}$ when restricted to the vertices reachable from $(p, \perp)$.

Consider the reachability game $(\mathcal{A}, \text{Reach}(\{0\}))$. Then, every vertex of the form $(q, \perp v)$ is winning for Eve and every vertex of the form $(p, \perp v)$ is winning for Adam as Adam can always choose to push a $\gamma$-symbol while remaining in state $p$ hence always avoiding the state $r$ (which is the only state with colour 0). If instead we consider, the Büchi game Buchi$(\{0,2\})$, then Eve is winning form all vertices. The strategy for Adam consisting in always pushing a $\gamma$-symbol while remaining in state $p$ results in a play that infinitely often sees the colour 2.

<figure><img src="image_80.png" /><figcaption>Figure 10.1: Pushdown arena from Example 6</figcaption></figure>

As a pushdown arena is in general infinite, the winning region for Eve, i.e., the set of winning vertices for Eve may not admit a finite presentation. Similarly, for objectives for which finite-memory strategies exists, the question of whether such a strategy can be finitely presented (and computed) is raised. Hence, we will in general distinguish the following three algorithmic problems.

**Problem 10** (Solving a pushdown game).

**INPUT:** A pushdown game $\mathcal{G}$ and an initial vertex $v_0$

**OUTPUT:** Does Eve win $\mathcal{G}$ from $v_0$?

**Problem 11** (Computing the winning region).

**INPUT:** A pushdown game $\mathcal{G}$

**OUTPUT:** Output a finite presentation of the set $v$ of vertices from which Eve wins $\mathcal{G}$

In Theorem 10.6, we will show that the winning region can be described by a finite-state automaton for a large class of qualitative winning conditions.

**Problem 12** (Computing a winning strategy).

**INPUT:** A pushdown game $\mathcal{G}$

**OUTPUT:** Output a finite presentation of a strategy for Eve that is winning from any vertex in the winning region for Eve in $\mathcal{G}$

We will show, for parity pushdown games, that the winning strategy can be described using either a finite-state automaton or a pushdown automaton (see Section 10.3.3).
## 10.2 Profiles and regularity of the winning regions

In this section, we consider a large class of objectives called *prefix independent*. For these objectives, a pushdown game can be meaningfully decomposed by considering the part of the game between the moment a symbol is pushed onto the stack and stopping as soon as it is popped. As a consequence, we will see that for prefix independent objectives, the winning region can be described using finite state automata.

To this extent, we introduce *reduced games* which start with a stack containing only one symbol $\gamma$ and stop as soon as this symbol is popped from the stack. If the symbol is never popped, the objective is unchanged and otherwise the winner of the game is determined by the state reached when popping the symbol.

Let $\mathcal{G} = (\mathcal{A}, \Omega)$ be a pushdown game played on an arena $\mathcal{A} = (G, V_{\text{Eve}}, V_{\text{Adam}})$ generated by a pushdown system $\mathcal{P} = (Q, Q_{\text{Eve}}, Q_{\text{Adam}}, \Gamma, \Delta)$. For any subset $R \subseteq Q$ of control states of $\mathcal{P}$, we define a new objective $\Omega(R)$ such that a play $\pi$ belongs to $\Omega(R)$ if one of the following happens:

* the play $\pi$ belongs to $\Omega$ and does not contain any configuration with an empty stack (i.e., of the form $(q, \perp)$ for some state $q \in Q$),

* the play $\pi$ contains a configuration with the empty stack and the first such configuration has a state in $R$.

More formally, letting $V = V_{\text{Eve}} \cup V_{\text{Adam}}$, $V_R = R \times \perp \Gamma^*$ and $V_{\perp} = Q \times \{\perp\}$

$$ \Omega(R) = (\Omega \setminus V^*V_{\perp}V^{\omega}) \cup (V \setminus V_{\perp})^*V_RV^{\omega} $$

Finally, we let $\mathcal{G}(R)$ denote the game $(\mathcal{A}, \Omega(R))$.

Remark that contrarily to the rest of the objectives considered in this chapter, $\Omega(R)$ does depend on the sequences of vertices visited by the play and not only on their colour. It would have been possible by a slight modification of the arena to only express the objective on their colours. However, our choice simplifies the presentation of the reduced games.

For any state $q \in Q$ and any stack letter $\gamma \in \Gamma$, we denote by $\mathcal{R}(q, \gamma)$ the set of subsets $R \subseteq Q$ for which Eve wins in $\mathcal{G}(R)$ from $(q, \perp \gamma)$:

$$ \mathcal{R}(q, \gamma) = \{R \subseteq Q \mid (q, \perp \gamma) \text{ is winning for Eve in } \mathcal{G}(R)\} $$

and we refer to $\mathcal{R}(q, \gamma)$ as the $(q, \gamma)$-profile of $\mathcal{G}$.

An objective $\Omega \subseteq C^\omega$ is *prefix independent* if the following holds: for every $u \in C^\omega$ and for every $v \in C^*$, $u \in \Omega$ if and only if $vu \in \Omega$. The Büchi, co-Büchi and parity objectives are examples of prefix independent objectives and the reachability objective is not.

**Remark 14.** For a prefix independent objective, a play respecting a winning strategy for Eve that starts in Eve's winning region always stays in this region. Obviously this is no longer true if the objective is not prefix independent. For instance in a reachability game, a play following a winning strategy for Eve can leave the winning region of Eve once the target has been reached.
This simple property allows to use profiles to give an inductive characterization of
the winning region for Eve when the objective is prefix independent.

**Proposition 4.** Assume that $\Omega \subseteq C^\omega$ is prefix independent. Let $s \in \Gamma^*$, $q \in Q$ and $\gamma \in \Gamma$. Then Eve has a winning strategy in $\mathcal{G}$ from $(q, \perp s\gamma)$ if and only if there exists some $R \in \mathcal{R}(q, \gamma)$ such that $(r, \perp s)$ is winning for Eve in $\mathcal{G}$ for every $r \in R$.

*Proof.* Assume Eve has a winning strategy $\sigma$ from $(q, \perp s\gamma)$ in $\mathcal{G}$. Consider the set $\Pi_\sigma$ of all plays in $\mathcal{G}$ that starts from $(q, \perp s\gamma)$ and where Eve respects $\sigma$. Define $R$ to be the (possibly empty) set that consists of all $r \in Q$ such that there is a play in $\Pi_\sigma$ of the form $v_0 \cdots v_k(r, \perp s)v_{k+1} \cdots$ where each $v_i$ for $0 \le i \le k$ is of the form $(p_i, \perp s t_i)$ for some non-empty $t_i$. In other words, $R$ consists of all states that can be reached on popping $\gamma$ for the first time in a play where Eve respects $\sigma$. As seen in Remark 14, Eve is winning from $(r, \perp s)$ for all $r \in R$. It remains to show that $R \in \mathcal{R}(q, \gamma)$.

To this end, define a (partial) function $\xi$ as $\xi((p, \perp st)) = (p, \perp t)$ for every $p \in Q$ and set $\xi^{-1}((p, \perp t)) = (p, \perp st)$. Then $\xi^{-1}$ is extended as a morphism over $V^*$. Now a winning strategy for Eve in $\mathcal{G}(R)$ is defined as follows:

* if some empty stack configuration has already been visited play any valid move,

* otherwise go to $\xi(\sigma(\xi^{-1}(\pi)))$, where $\pi$ is the current play.

By definition of $\Pi_\sigma$ and $R$, it easily follows that the previous strategy is winning for
Eve in $\mathcal{G}(R)$, and therefore $R \in \mathcal{R}(p, \gamma)$.

Conversely, let us assume that there is some $R \in \mathcal{R}(q, \gamma)$ such that $(r, \perp s)$ is winning for Eve in $\mathcal{G}$ for every $r \in R$. For every $r \in R$, let us denote by $\sigma_r$ a winning strategy for Eve from $(r, \perp s)$ in $\mathcal{G}$. Let $\sigma_R$ be a winning strategy for Eve in $\mathcal{G}(R)$ from $(q, \perp \gamma)$. Let us define $\xi$ and $\xi^{-1}$ as in the direct implication and extend them as (partial) morphism over $V^*$. Define the following strategy $\sigma$ for Eve in $\mathcal{G}$ for plays starting from $(q, \perp s\gamma)$. For any such play $\pi$,

* if $\pi$ does not contain a configuration of the form $(p, \perp s)$ then we take $\sigma(\pi) = \xi^{-1}(\sigma_R(\xi(\pi)))$;

* otherwise let $\pi = \pi' \cdot (r, \perp s) \cdot \pi''$ where $\pi'$ does not contain any configuration of the form $(p, \perp s)$. If $r$ does not belong to $R$, $\sigma$ is undefined. Note that this situation will never be encountered in a play respecting $\sigma$ as $\sigma_R$ ensures that $r \in R$. If $r \in R$, one finally sets $\sigma(\pi) = \sigma_r((r, \perp s)\pi'')$.

The strategy $\sigma$ is a winning strategy for Eve in $\mathcal{G}$ from $(q, \perp s\gamma)$. To see this, consider a play $\pi$ starting from $(p, \perp s\gamma)$ and respecting $\sigma$.

If the play $\pi$ does not contain configurations of the form $(r, \perp s)$ for some $r \in Q$,
then the play $\xi(\pi)$ starting in $(p, \perp \gamma)$ respects $\sigma_R$ and is won by Eve. As $\xi(\pi)$ does
not contain configurations with an empty stack, it must be the case that $\xi(\pi) \in \Omega$. As
$\Omega$ only depends on the colours of the states, it is also the case that $\pi \in \Omega$ and hence, $\pi$
is winning for Eve.

If the play $\pi$ can be decomposed as $\pi'(r, \perp s)\pi''$ where $\pi'$ does not contain any configuration with the stack $\perp s$, the play $\xi(\pi'(r, \perp s))$ respects $\sigma_R$ in $\mathcal{G}(R)$. As $\sigma_R$ is winning, it follows that $r \in R$. By definition of $\sigma$, $(r, \perp s)\pi''$ respects $\sigma_r$ which being
winning for Eve implies that $(r, \perp s)\pi'' \in \Omega$. As $\Omega$ is prefix independent, it follows that $\pi \in \Omega$. $\square$

Proposition 4 implies that the winning region of any pushdown game equipped with a prefix independent objectives can be described by regular languages.

**Theorem 106.** Let $\mathcal{G} = (\mathcal{A}, \Omega)$ be a pushdown game played on an arena $\mathcal{A} = (G, V_{Eve}, V_{Adam})$ generated by a pushdown system $\mathcal{P} = (Q, Q_{Eve}, Q_{Adam}, \Gamma, \Delta)$, and such that $\Omega \subseteq C^\omega$ is prefix independent. Then for any state $q \in Q$, the set

$$L_q = \{u \in \Gamma^* | (q, \perp u) \in W_{Eve}\}$$

is a regular language over the alphabet $\Gamma$.

*Proof.* Fix a control state $q \in Q$, we consider a deterministic finite state automaton defined as follows. Its set of control states consists of the subsets of $Q$ and the initial state is $S_{in} = \{p \mid (p, \perp) \in W_{Eve}\}$. From the state $S$ upon reading the letter $\gamma$ the automaton goes to the state $\{p \mid S \in \mathcal{R}(p, \gamma)\}$. Finally a state $S$ is final if and only if $q \in S$. It is then an immediate consequence of Proposition 4 that this automaton accepts the language $L_q$. $\square$

**Remark 15.** By a slight abuse, we can think of the $|Q|$ automata in Theorem 106 as a single automaton that is designed to first read the stack content and finally reads the control state $q$ (in this latter step, from state $S$ it either goes to a final state if $q \in S$ or to a rejecting one otherwise).

**Remark 16.** Note that the characterisation in Theorem 106 is a priori not effective. Indeed, to construct automata for the languages $L_q$ one needs to be able to compute all the $(q, \gamma)$-profiles $\mathcal{R}(q, \gamma)$ of $\mathcal{G}$ and compute the winner from configurations of the form $(q, \perp)$.

Consider, for instance, the objective over the set of the colours $C = \{0, 1, \#, \$\}$

$$\Omega_{pal} = \{w \in C^\omega \mid w \text{ contains infinitely many factors of the form } \#u\$\bar{u}\# \text{ with } u \in \{0, 1\}^*\}$$

where $\bar{u}$ denotes the mirror of the word $u$.

As a language of $\omega$-words, this objective is accepted by a deterministic $\omega$-pushdown automaton with a Büchi acceptance condition. Between two consecutive occurrences of the $\#$-symbol, the automaton checks that the word $w$ appearing in between these two occurrences is of the form $u\$\bar{u}$ for some word $u \in \{0, 1\}^*$. This can be done in a deterministic manner as follows. First the automaton pushes onto the stack a symbol $\perp'$ (which will play the same role as the bottom of stack symbol) then it pushes onto the stack all symbols in $\{0, 1\}$ that are read. Then when the first $\$-symbol is read, it only allows to read the symbol that is on the top of the stack before popping it. Finally when a $\#$-symbol is read, if the top-most symbol of the stack is $\perp'$ the unique final state is visited. Hence ensuring that a final state is visited if the word $w$ is of the required form. If $w$ contains several $\$-symbols or if the symbol read does not correspond to the top of the stack, the automaton enters a non-final state is in which it waits for the next $\#$-symbol.
For games with finite arenas and the $\Omega_{pal}$ objective, deciding the winner reduces to deciding the winner in a pushdown game with the Büchi objective which is decidable as we will prove later in this chapter. The pushdown game is essentially a synchronized product between the finite arena and the $\omega$-pushdown automaton described previously.

However the problem of deciding the winner in a pushdown game with the $\Omega_{pal}$ objective is undecidable even if all vertices belong to Eve. The undecidability is proved by a reduction from Post correspondence problem (PCP) which is a well-known to be undecidable. Recall that an instance of PCP is a finite sequence $(r_1, \ell_1), \dots, (r_n, \ell_n)$ of pairs of words over $\{0,1\}$. Such an instance is said to admit a solution if there exists a sequence of indices $i_1 \cdots i_k \in [1,n]^*$ such that:

$$r_{i_1} r_{i_2} \cdots r_{i_k} = \ell_{i_1} \ell_{i_2} \cdots \ell_{i_k}.$$

The PCP problem is, given an instance, to decide if it admits a solution.

For an instance $I = (\ell_1, r_1), \dots, (\ell_n, r_n)$ of PCP, we construct a pushdown game $G_I$ with the objective $\Omega_{pal}$ such that Eve wins $G_I$ from $(p_*, \perp)$ if and only if $I$ admits a solution. In this game, Eve plays alone and the play is decomposed in two phases that will repeat:

* in phase 1, Eve can push any index $i$ in $[1,n]$ while producing the sequence of colors $r_i$. As soon as at least one index has been pushed, she can also choose to move to the sequence phase while producing the colour $\$$.

* in phase 2, Eve must (until the bottom of stack symbol is reached) pop the top most element of the stack $i$ while producing the sequence of colours $\tilde{l}_i$. When the bottom of stack symbol is encountered, Eve goes back to the first phase while producing the colour $\#$$.

If $I$ has a solution $i_1 \cdots i_k$ then the strategy in which Eve always pushes this sequence in phase 1 is winning for her. As $i_1 \cdots i_k$ is a solution of $I$, we have $u = r_{i_1} \cdots r_{i_k} = \ell_{i_1} \cdots \ell_{i_k}$ and by construction of the game, the sequence of colors associated with the play is $(u\$\tilde{u})^\omega \in \Omega_{pal}$. Conversely if Eve has a winning strategy from $(q_*, \perp)$ then the sequence of colours associated with the winning play belongs to $\Omega_{pal}$. In particular, it must contain a factor of the form $\#u\$\tilde{u}\#$. By construction of the game the sequence of indices $i_1 \cdots i_k$ pushed while producing $u$ is a solution of $I$.

### 10.2.1 Reachability Pushdown Game

We will see in the following section that for the parity condition and more generally for any $\omega$-regular winning conditions the $(q, \gamma)$-profiles can be computed for any $q \in \mathbb{Q}$ and $\gamma \in \Gamma$. We start by the simpler case of the reachability objective.

At first sight, the reachability objective is not captured by Theorem 106 as it is not prefix independent. However with a slight adaptation of the reduced game $\mathcal{G}(R)$ Theorem 106 for the reachability condition. Intuitively we ask that the play stops as soon as a target vertex is reached.

More formally, for a reachability objective $\text{Reach}(F)$ and letting $V = V_{\text{Eve}} \cup V_{\text{Adam}}$ and $V_F = \{v \in V \mid c(v) \in F\}$:

$$\overline{\Omega}(R) = [(V \setminus Q \times \{\perp\})^* \cdot V_F \cdot V^\omega] \cup [(V \setminus (Q \times \{\perp\} \cup V_F))^* \cdot (R \times \{\perp\}) \cdot V^\omega]$$
It is easily shown that with this modification to the definition of profiles both Proposition 4 and Theorem 106 are true for the reachability objective. In the special case of the reachability objective, the set Profs of triples $(p, \gamma, R)$ such that $R \in \mathcal{R}(p, \gamma)$ can be expressed as a smallest fixed point.

More precisely, Profs is the smallest subset of $Q \times \Gamma \times \mathcal{P}(Q)$ such that for $p \in Q$, $\gamma \in \Gamma$ and $R \subseteq Q$, $(p, \gamma, R)$ belongs Profs if either:

1. $p \in Q_F = \{q \in Q \mid c(q) \in F\}$,

2. or $p \in Q_{Eve}$ and for some $q \in Q$,

• either $(q, \text{pop}) \in \Delta(p, \gamma)$ and $q \in R$,

• or $(q, \text{push}(\gamma')) \in \Delta(p, \gamma)$ and $(q, \gamma', R') \in \text{Profs}$ for some $R' \subseteq Q$ such that for all $p' \in R'$, $(p', \gamma, R) \in \text{Profs}$.

3. or $p \in Q_A$ and for all $q \in Q$ the following hold:

• $(q, \text{pop}) \in \Delta(p, \gamma)$ implies $q \in R$,

• $(q, \text{push}(\gamma')) \in \Delta(p, \gamma)$ implies that there exists $R' \subseteq Q$ such that $(q, \gamma', R') \in \text{Profs}$ and for all $p' \in R'$, $(p', \gamma, R) \in \text{Profs}$.

Using this characterization, the set Profs can be computed using the standard method for computing small-fixed point of a monotonic function by computing the sequence of approximants $\text{Profs}_0 = \emptyset \subseteq \text{Profs}_1 \subseteq \text{Profs}_2 \cdots$ until it stabilizes. More precisely, for all $i \ge 0$, $\text{Profs}_{i+1}$ is obtained by adding to $\text{Profs}_i$ all the tuples that can be inferred using the properties (1), (2) and (3) above applied to $\text{Profs}_i$. As at most $|Q| \cdot |\Gamma| \cdot 2^{|Q|}$ tuples can be added, the sequence must stabilize in at most $|Q| \cdot |\Gamma| \cdot 2^{|Q|}$ steps. As the computation of $\text{Profs}_{i+1}$ from $\text{Profs}_i$ can be performed in polynomial time, the profiles in a reachability pushdown game can be computed in time $p(|Q| \cdot |\Gamma| \cdot 2^{|Q|})$ for some polynomial $p$.

**Remark 17.** In the case where Eve plays alone (i.e., $Q = Q_{Eve}$), there is only on play respecting a fixed strategy for Eve and as a result, one only need to compute profiles of the form $(p, \gamma, R)$ with $|R| \le 1$. In this setting, the fixed point characterization yields a polynomial time algorithm to compute the set of profiles.

## 10.3 Parity pushdown games

We now focus on the central case of parity objectives. In Section 10.3.1, we show how to compute the set of profiles using a reduction to finite parity game.

For the rest of this section, we fix a parity pushdown game $\mathcal{G}$ played on an arena $\mathcal{A} = (G, V_{Eve}, V_{Adam})$ generated by a pushdown system $\mathcal{P} = (Q, Q_{Eve}, Q_{Adam}, \Gamma, \Delta)$. We also let $V = V_{Eve} \cup V_{Adam}$ and we let the colours used in the game be $\{0, \dots, d\}$.
### 10.3.1 Computing the Profiles

In this section we show how to build a parity game played on a finite arena that permits to compute the profiles in $\mathcal{G}$.

We first start with some terminology and a basic result. For an infinite play $\pi = v_0v_1\cdots$, let $Steps_\pi$ be the set of indices of positions where no configuration of strictly smaller stack height is visited later in the play. More formally,

$$Steps_\pi = \{i \in \mathbb{N} | \forall j \ge i, \mathrm{sh}(v_j) \ge \mathrm{sh}(v_i)\}.$$

Note that $Steps_\pi$ is always infinite and hence induces a factorisation of the play $\pi$ into finite pieces.

In the factorisation induced by $Steps_\pi$, a factor $v_i \cdots v_j$ is called a *bump* if $\mathrm{sh}(v_j) = \mathrm{sh}(v_i)$, called a *Stair* otherwise (that is, if $\mathrm{sh}(v_j) = \mathrm{sh}(v_i) + 1$).

For any play $\pi$ with $Steps_\pi = \{n_0 < n_1 < \cdots\}$, we can define the sequence $(c(\pi)_i)_{i \ge 0} \in \{0, \dots, d\}^N$ by setting $c(\pi)_i = \max\{c(v_k) | n_i \le k \le n_{i+1}\}$. This sequence fully characterises the parity objective.

**Proposition 5.** Let $\pi$ be a play. Then $\pi$ satisfies the parity condition if and only if $\limsup((c(\pi)_i)_{i \ge 0})$ is even.

#### Simulation Game

In the sequel, we build a new parity game $\tilde{\mathcal{G}}$ over a finite arena $\tilde{\mathcal{A}}$. This new game simulates the original pushdown game, in the sense that the sequence of visited colours during a correct simulation of some play $\pi$ in $\mathcal{G}$ is exactly the sequence $(c(\pi)_i)_{i \ge 0}$. Moreover, a play in which a player does not correctly simulate the pushdown game is losing for that player. We shall see that the winning region in $\tilde{\mathcal{G}}$ allows us to compute the set of profiles $\{\mathcal{R}(q, \gamma) | q \in Q \text{ and } \gamma \in \Gamma\}$. Hence, by Theorem 106, it will imply that one can solve a pushdown game as well as compute its winning region.

Before providing a precise description of the arena $\tilde{\mathcal{A}}$, let us consider the following informal description of this simulation game. We aim at simulating a play in the push-down game from some initial vertex $(p_{in}, \perp)$. In $\tilde{\mathcal{A}}$ we keep track of only the control state and the top stack symbol of the currently simulated configuration.

The interesting case is when it is in a control state $p$ with top stack symbol $\alpha$, and the player owning $p$ wants to push a symbol $\beta$ onto the stack and change the control state to $q$. For every strategy of Eve, there is a certain set of possible (finite) continuations of the play that will end with popping $\beta$ from the stack. We require Eve to declare a vector $\vec{S} = (S_0, \dots, S_d)$ of $(d+1)$ subsets of $Q$, where $S_i$ is the set of all states the game can be in after popping $\beta$ along those plays where in addition the largest visited colour while $\beta$ was on the stack is $i$.

Adam has then two choices. He can continue the game by pushing $\beta$ onto the stack and updating the state (we call this a *pursue move*). Otherwise, he can pick a set $S_i$ and a state $r \in S_i$, and continue the simulation from that state $r$ (we call this a *jump move*). If he does a pursue move, then he remembers the vector $\vec{S}$ claimed by Eve; if later on, a pop transition is simulated, the play goes in a sink vertex and Evewins if and only if the resulting state is in $S_c$ where $c$ is the largest colour seen in the current stack level
<figure><img src="image_81.png" /><figcaption>Figure 10.2: Local structure of the arena $\tilde{\mathcal{A}}$</figcaption></figure>

(this information is encoded in the vertex, reset after each pursue move and updated after each jump move). If Adamdoes a jump move to a state $r$ in $S_i$, the currently stored value for $c$ is updated to $\max(c, i, c(r))$, which is the largest colour seen since the current stack level was reached.

Therefore the main vertices of this new arena are of the form $(p, \alpha, \vec{R}, c)$, which are controlled by the player who controls $p$. Intermediate vertices are used to handle the previously described intermediate steps. The local structure is given in Figure 10.2. Two special sink vertices $tt$ and $ff$ are used to simulate pop moves. This arena is equipped with a colouring function on the edges: an edge from a vertex $(p, \alpha, \vec{R}, c, q, \beta, \vec{S})$ to a vertex $(r, \alpha, \vec{R}, \max(c, i, c(r)))$ has colour $i$ where $i$ is the colour of the simulated bump, an edge from a vertex $(p, \alpha, \vec{R}, c, q, \beta, \vec{S})$ to a vertex $(q, \beta, \vec{S}, \max(c, i, c(r)))$ simulating a jump move has colour $c(q)$, the loop on $tt$ has colour 0 while the loop on $ff$ has colour 1; all other edges get the irrelevant colour 0.

We now formally describe arena $\tilde{\mathcal{A}}$ (we refer to Figure 10.2) and provide some extra insight.

* The main vertices of $\tilde{\mathcal{A}}$ are those of the form $(p, \alpha, \vec{R}, c)$, where $p \in Q$, $\alpha \in \Gamma$, $\vec{R} = (R_0, \dots, R_d) \in (2^Q)^{d+1}$ and $c \in \{0, \dots, d\}$. A vertex $(p, \alpha, \vec{R}, c)$ is reached when simulating a finite play $\pi$ in $\mathcal{G}$ such that:
- The last vertex in $\pi$ is $(p, \perp s\alpha)$ for some $s \in \Gamma^*$.

- Eve claims that she has a strategy to continue $\pi$ in such a way that if $\alpha$ is eventually popped, the control state reached after popping belongs to $R_m$, where $m$ is the largest colour visited since the stack height was at least $|s\alpha|$.

- The colour $c$ is the largest one since the current stack level was reached from a lower stack level.

A vertex $(p, \alpha, \vec{R}, c)$ is controlled by Eve if and only if $p \in Q_{Eve}$.

* The vertices $tt$ and $ff$ are here to ensure that the vectors $\vec{R}$ encoded in the main vertices are correct. They are both controlled by Eve and are sink vertices with a self loop with colour 0 for $tt$ and 1 for $ff$.

There is a transition from some vertex $(p, \alpha, \vec{R}, c)$ to $tt$, if and only if there exists a transition rule $(r, pop) \in \Delta(p, \alpha)$, such that $r \in R_c$ (this means that $\vec{R}$ is correct with respect to this transition rule). Dually, there is a transition from a vertex $(p, \alpha, \vec{R}, c)$ to $ff$ if and only if there exists a transition rule $(r, pop) \in \Delta(p, \alpha)$ such that $r \notin R_c$ (this means that $\vec{R}$ is not correct with respect to this transition rule).

* To simulate a transition rule $(q, push(\beta)) \in \Delta(p, \alpha)$, the player that controls $(p, \alpha, \vec{R}, c)$ moves to $(p, \alpha, \vec{R}, c, q, \beta)$. This vertex is controlled by Eve who has to give a vector $\vec{S} = (S_0, \dots, S_d) \in (2^Q)^{d+1}$ that describes the control states that can be reached if $\beta$ is eventually popped. To describe this vector, she goes to the corresponding vertex $(p, \alpha, \vec{R}, c, q, \beta, \vec{S})$.

Any vertex $(p, \alpha, \vec{R}, c, q, \beta, \vec{S})$ is controlled by Adam who chooses either to simulate a bump or a stair. In the first case, he additionally has to pick the maximal colour of the bump. To simulate a bump with maximal colour $i$, he goes, through an edge coloured by $i$, to a vertex $(r, \alpha, \vec{R}, \max(c, i, c(r)))$, for some $r \in S_i$.

To simulate a stair, Adam goes, through an edge coloured by $c(q)$, to the vertex $(q, \beta, \vec{S}, c(q))$.

The last component of the vertex (that stores the largest colour seen since the currently simulated stack level was reached) has to be updated in all those cases. After simulating a bump of maximal colour $i$, the maximal colour is $\max(c, i, c(r))$. After simulating a stair, this colour has to be initialized (since a new stack level is simulated). Its value, is therefore $c(q)$, which is the unique colour since the (new) stack level was reached.

The edges for which we did not precise the colour are assigned colour 0.

The following theorem relates this new game $\tilde{\mathcal{G}}$ and the profiles in the pushdown game $\mathcal{G}$.

**Theorem 107.** *The following holds.*
(i) A configuration $(p_{in}, \perp)$ is winning for Eve in $\mathcal{G}$ if and only if $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$ is winning for Eve in $\mathcal{G}$.

(ii) For every $q \in \mathcal{Q}$, $\gamma \in \Gamma$ and $R \subseteq \mathcal{Q}$, $R \in \mathcal{R}(q, \gamma)$ if and only if $(q, \gamma, (R, \dots, R), c(q))$ is winning for Eve in $\tilde{\mathcal{G}}$.

The rest of the section is devoted to the proof of Theorem 107. We only prove point (i) as the proof of point (ii) is a subpart of the proof of (i).

**Factorisation of a play in $\mathcal{G}$**

Recall that, for an infinite play $\pi = v_0v_1\cdots$ in $\mathcal{G}$, $\text{Steps}_\pi$ denotes the set of indices of positions where no configuration of strictly smaller stack height is visited later in the play. Note that $\text{Steps}_\pi$ is always infinite and hence induces a factorisation of the play $\pi$ into finite pieces.

Indeed, for any play $\pi$ with $\text{Steps}_\pi = \{n_0 < n_1 < \cdots\}$, one can define the sequence $(\pi_i)_{i \ge 0}$ by setting $\pi_i = v_{n_i} \cdots v_{n_{i+1}}$. Note that each of the $\Lambda_i$ is either a bump or a stair. We designate $(\pi_i)_{i \ge 0}$ as the *rounds factorisation* of $\pi$ and we let $c(\pi_i)$ denotes the largest colour in $\pi_i$.

**Factorisation of a play in $\tilde{\mathcal{G}}$**

Recall that in $\tilde{\mathcal{A}}$ only some edges have a relevant colour while all others get colour 0. Hence, to represent a play, we only keep the relevant colours of edges. More precisely, we only need to encode the colours in $\{0, \dots, d\}$ that appears when simulating a bump: a play will be represented as a sequence of vertices together with colours in $\{0, \dots, d\}$ that correspond to (relevant) colours appearing on edges.

For any play in $\tilde{\mathcal{G}}$, a *round* is a factor between two visits through vertices of the form $(p, \alpha, \vec{R}, c)$. We have the following possible forms for a round:

* The round is of the form

$$ (p, \alpha, \vec{R}, c)(p, \alpha, \vec{R}, c, q, \beta)(p, \alpha, \vec{R}, c, q, \beta, \vec{S})i(r, \alpha, \vec{R}, \max(c, i, c(s))) $$

and corresponds therefore to the simulation of a rule pushing $\beta$ followed by a sequence of moves that ends by popping $\beta$. Moreover $i$ is the largest colour encountered while $\beta$ was on the stack.

* The round is of the form

$$ (p, \alpha, \vec{R}, c)(p, \alpha, \vec{R}, c, q, \beta)(p, \alpha, \vec{R}, c, q, \beta, \vec{S})c(q)(q, \beta, \vec{S}, c(q)) $$

and corresponds therefore to the simulation of a rule pushing a symbol $\beta$ leading to a new stack level below which the play will never go. We designate it as a *stair*.
For any play $\tilde{\pi} = v_0v_1v_2\cdots$ in $\mathcal{G}$, we consider the subset of indices corresponding
to vertices of the form $(p, \alpha, \vec{R}, c)$. More precisely:

$$
\text{Rounds}_{\tilde{\pi}} = \{n \mid v_n = (p, \alpha, \vec{R}, c), p \in Q, \alpha \in \Gamma, \vec{R} \in (2^Q)^{d+1}, 0 \le c \le d\}
$$

Therefore, the set $\text{Rounds}_{\tilde{\pi}}$ induces a natural factorisation of $\tilde{\pi}$ into rounds.

**Definition 29 (Rounds factorisation).** For a (possibly finite) play $\tilde{\pi} = v_0v_1v_2\cdots$, we call rounds factorisation of $\tilde{\pi}$, the (possibly finite) sequence $(\tilde{\pi}_i)_{i\ge 0}$ of rounds defined as follows. Let $\text{Rounds}_{\tilde{\pi}} = \{n_0 < n_1 < n_2 < \cdots\}$, then for all $0 \le i < |\text{Rounds}_{\tilde{\pi}}|$, define $\tilde{\pi}_i = v_{n_i} \cdots v_{n_{i+1}}$.

Therefore, for every $i \ge 0$, the first vertex in $\tilde{\pi}_{i+1}$ equals the last one in $\tilde{\pi}_i$. Moreover,
$\tilde{\pi} = \tilde{\pi}_1 \odot \tilde{\pi}_2 \odot \tilde{\pi}_3 \odot \dots$, where $\tilde{\pi}_i \odot \tilde{\pi}_{i+1}$ denotes the concatenation of $\tilde{\pi}_i$ with $\tilde{\pi}_{i+1}$
without its first vertex. Finally, the colour of a round is the unique colour in $\{0, \dots, d\}$
appearing in the round.

In order to prove both implications of Theorem 107, we build from a winning
strategy for Eve in one game a winning strategy for her in the other game. The main ar-
gument to prove that the new strategy is winning is to prove a correspondence between
the factorisations of plays in both games.

**Proof of the Direct Implication of Theorem 107**

Assume that the configuration $(p_{in}, \perp)$ is winning for Eve in $\mathcal{G}$, and let $\sigma$ be a corre-
sponding winning strategy for her.

Using $\sigma$, we define a strategy $\tilde{\sigma}$ for Eve in $\tilde{\mathcal{G}}$ from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$. This
strategy stores a finite play in $\mathcal{G}$, that is an element in $V^*$. This memory will be denoted
$\pi$. At the beginning $\pi$ is initialized to the vertex $(p_{in}, \perp)$. We first describe $\tilde{\sigma}$, and then
we explain how $\pi$ is updated. Both the strategy $\tilde{\sigma}$ and the update of $\pi$, are described
for a round.

**Choice of the move.** Assume that the play is in some vertex $(p, \alpha, \vec{R}, c)$ for $p \in Q_{\text{Eve}}$. The move given by $\tilde{\sigma}$ depends on $\sigma(\pi)$:

* If $\sigma(\pi) = (r, pop)$, then Eve goes to $t$ (Proposition 6 will prove that this move is always possible).

* If $\sigma(\pi) = (q, push(\beta))$, then Eve goes to $(p, \alpha, \vec{R}, c, q, \beta)$.

In this last case, or in the case where $p \in Q_{\text{Adam}}$ and Adam goes to $(p, \alpha, \vec{R}, c, q, \beta)$,
we also have to explain how Eve behaves from $(p, \alpha, \vec{R}, c, q, \beta)$. She has to provide
a vector $\vec{S} \in (2^Q)^{d+1}$ that describes which states can be reached if $\beta$ is eventually
popped, depending on the largest colour visited in the meantime. In order to define
$\vec{S}$, Eve considers the set of all possible continuations of $\pi \cdot (q, s\alpha\beta)$ (where $(p, s\alpha)$
denotes the last vertex of $\pi$) where she respects her strategy $\sigma$. For each such play,
she checks whether some configuration of the form $(r, s\alpha)$ is visited after $\pi \cdot (q, s\alpha\beta)$,
that is if the stack level of $\beta$ is eventually left. If it is the case, she considers the first
configuration $(r, s\alpha)$ appearing after $\pi \cdot (q, \sigma\alpha\beta)$ and the largest colour $i$ since $\beta$ was
on the stack. For every $i \in \{0, \dots, d\}$, $S_i$, is exactly the set of states $r \in Q$ such that the preceding case happens. More formally,

$$S_i = \{r \mid \exists \pi \cdot (q, s\alpha\beta)v_0 \cdots v_k(r, s\alpha) \cdots \text{play in } \mathcal{G} \text{ where Eve respects } \sigma \text{ and s.t.} \\ \qquad \text{sh}(v_j) > |\sigma\alpha|, \forall j = 0, \dots, k, \text{ and } \max(\{c(v_j) \mid j = 0, \dots, k\} \cup \{c(q)\}) = i\}$$

Finally, we set $\vec{S} = (S_0, \dots, S_d)$ and Eve moves to $(p, \alpha, \vec{R}, c, q, \beta, \vec{S})$.

**Update of $\pi$.** The memory $\pi$ is updated after each visit to a vertex of the form $(p, \alpha, \vec{R}, c)$. We have two cases depending on the kind of the last round:

* The round is a bump, and therefore a bump of colour $i$ (where $i$ is the colour of the round) starting with some transition $(q, push(\beta))$ and ending in a state $r \in S_i$ was simulated. Let $(p, s\alpha)$ be the last vertex in $\pi$. Then the memory becomes $\pi$ extended by $(q, s\alpha\beta)$ followed by a sequence of moves, where Eve respects $\sigma$, that ends by popping $\beta$ and reach $(r, s\alpha)$ while having $i$ as largest colour. By definition of $S_i$ such a sequence of moves always exists.

* The round is a stair and therefore we have simulated a transition $(q, push(\beta))$. If $(p, s\alpha)$ denotes the last vertex in $\pi$, then the updated memory is $\pi \cdot (q, s\alpha\beta)$.

Therefore, with any finite play $\tilde{\pi}$ in $\tilde{\mathcal{G}}$ in which Eve respects her strategy $\tilde{\sigma}$, is associated a finite play $\pi$ in $\mathcal{G}$. An immediate induction shows that Eve respects $\sigma$ in $\pi$. The same arguments works for an infinite play $\tilde{\pi}$, and the corresponding play $\pi$ is therefore infinite, starts from $(p_{in}, \perp)$ and Eve respects $\sigma$ in that play. Therefore it is a winning play.

The following proposition is a direct consequence of how $\tilde{\sigma}$ was defined.

**Proposition 6.** Let $\tilde{\pi}$ be a finite play in $\tilde{\mathcal{G}}$ that starts from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$, ends in a vertex of the form $(p, \alpha, \vec{R}, c)$, and where Eve respects $\tilde{\sigma}$. Let $\pi$ be the play associated with $\tilde{\pi}$ built by the strategy $\tilde{\sigma}$. Then the following holds:

1. $\pi$ ends in a vertex of the form $(p, s\alpha)$ for some $s \in \Gamma^*$.

2. $c$ is the largest colour visited in $\pi$ since $\alpha$ was pushed.

3. Assume that $\pi$ is extended, that Eve keeps respecting $\sigma$ and that the next move after $(p, \sigma\alpha)$ is to some vertex $(r, \sigma)$. Then $r \in R_c$.

Proposition 6 implies that the strategy $\tilde{\sigma}$ is well defined when it provides a move to $tt$. Moreover, one can deduce that, if Eve respects $\tilde{\sigma}$, $ff$ is never reached.

For plays that do not visits $tt$ nor $ff$, using the definitions of $\tilde{\mathcal{A}}$ and $\tilde{\sigma}$, we easily deduce the following proposition.

**Proposition 7.** Let $\tilde{\pi}$ be an infinite play in $\tilde{\mathcal{G}}$ that starts from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$, and where Eve respects $\tilde{\sigma}$. Let $\pi$ be the associated play built by the strategy $\tilde{\sigma}$, and let $(\tilde{\pi}_i)_{i \ge 0}$ be its rounds factorisation. Let $(\tilde{\pi}_i)_{i \ge 0}$ be the rounds factorisation of $\tilde{\pi}$. Then, for every $i \ge 1$ the following hold:
1. $\tilde{\pi}_i$ is a bump if and only if $\pi_i$ is a bump

2. $\tilde{\pi}_i$ has colour $c(\pi_i)$.

Proposition 7 implies that for any infinite play $\tilde{\pi}$ in $\tilde{\mathcal{G}}$ starting from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$ where Eve respects $\tilde{\sigma}$, the sequence of visited colours in $\tilde{\pi}$ is $(c(\pi)_i)_{i \ge 0}$ for the corresponding play $\pi$ in $\mathcal{G}$. Hence, using Proposition 5 we conclude that $\tilde{\pi}$ is winning if and only if $\pi$ is winning. As $\pi$ is winning for Eve, it follows that $\tilde{\pi}$ is also winning for her.

**Proof of the Converse Implication of Theorem 107**

Note that in order to prove the converse implication of Theorem 107 one could follow the direct implication and consider the point of view of Adam. Nevertheless the proof we give here starts from a winning strategy for Eve in $\tilde{\mathcal{G}}$ and deduces a strategy for her in $\mathcal{G}$: this induces a more involved proof but has the advantage to lead to an effective construction of a winning strategy for Eve in $\mathcal{G}$ if one has an effective strategy for her in $\tilde{\mathcal{G}}$.

Assume now that Eve has a winning strategy $\tilde{\sigma}$ in $\tilde{\mathcal{G}}$ from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$. Using $\tilde{\sigma}$, we build a strategy $\sigma$ for Eve in $\mathcal{G}$ for plays starting from $(p_{in}, \perp)$.

The strategy $\sigma$ uses, as memory, a stack $\Pi$, to store the complete description of a play in $\tilde{\mathcal{G}}$. Recall here that a play in $\tilde{\mathcal{G}}$ is represented as a sequence of vertices together with colours in $\{0, \dots, d\}$. Up to coding we can assume that we distinguish for free between stairs and bumps for transitions from vertices of the form $(p, \alpha, \vec{R}, c, q, \beta, \vec{S})$.

The stack alphabet of $\Pi$ is the set of vertices of $\tilde{\mathcal{A}}$ together with the colours $\{0, \dots, d\}$. In the following, $\text{top}(\Pi)$ will denote the top stack symbol of $\Pi$ while $\text{StCont}(\Pi)$ will be the word obtained by reading $\Pi$ from bottom to top (without considering the bottom-of-stack symbol of $\Pi$). In any play where Eve respects $\sigma$, $\text{StCont}(\Pi)$ will be a play in $\tilde{\mathcal{G}}$ that starts from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$ and where Eve respects her winning strategy $\tilde{\sigma}$. Moreover, for any play $\pi$ where Eve respects $\sigma$, we will always have that $\text{top}(\Pi) = (p, \alpha, \vec{R}, c)$ if and only if the current configuration in $\pi$ is of the form $(p, s\alpha)$. Finally, if Eve keeps respecting $\sigma$, and if $\alpha$ is eventually popped the configuration reached will be of the form $(r, s)$ for some $r \in \mathcal{R}_i$, where $i$ is the largest visited colour since $\alpha$ was on the stack. Initially, $\Pi$ only contains $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$.

In order to describe $\sigma$, we assume that we are in some configuration $(p, s\alpha)$ and that $\text{top}(\Pi) = (p, \alpha, \vec{R}, c)$. We first describe how Eve plays if $p \in \mathcal{Q}_{\text{Eve}}$, and then we explain how the stack is updated.

* **Choice of the move.** Assume that $p \in \mathcal{Q}_{\text{Eve}}$ and that Eve has to play from some vertex $(p, s\alpha)$. For this, she considers the value of $\tilde{\sigma}$ on $\text{StCont}(\Pi)$.

If it is a move to $\ell t$, Eve plays a transition $(r, \text{pop})$ for some state $r \in \mathcal{R}_c$. Lemma 130 will prove that such an $r$ always exists.

If the move given by $\tilde{\sigma}$ is to go to some vertex $(p, \alpha, \vec{R}, c, q, \beta)$, then Eve applies the transition $(q, \text{push}(\beta))$.
• Update of Π. Assume that the last move, played by Eve or Adam, was to go from (p, sα) to some configuration (r, s). The update of Π is illustrated by Figure 10.3 and explained in what follows. Eve pops in Π until she finds some configuration of the form (p', α', $\vec{R}'$, c', p'', α, $\vec{R}$) that is part of a stair. This configuration is therefore in the stair that simulates the pushing of α onto the stack. Eve updates Π by pushing c in Π followed by (r, α', $\vec{R}'$, max(c', c, c(r))).

Assume that the last move, played by Eve or Adam, was to go from (p, sα) to some configuration (q, sαβ), and let (p, α, $\vec{R}$, c, q, β, $\vec{s}$) = $\tilde{\sigma}$(StCont(Π) · (p, α, $\vec{R}$, c, q, β)). Intuitively, $\vec{s}$ describes which states Eve can force a play to reach if β is eventually popped. Eve updates Π by successively pushing (p, α, $\vec{R}$, c, q, β), (p, α, $\vec{R}$, c, q, β, $\vec{s}$), and (q, β, $\vec{s}$, c(q)).

The following lemma gives the meaning of the information stored in Π.

**Lemma 130.** Let $\pi$ be a finite play in $\mathcal{G}$, where Eve respects $\sigma$, that starts from $(p_{in}, \perp)$ and that ends in a configuration $(p, s\alpha)$. We have the following facts:

1. $\text{top}(\Pi) = (p, \alpha, \vec{R}, c)$ with $\vec{R} \in (2^Q)^{d+1}$ and $0 \le c \le d$.

2. StCont(Π) is a finite play in $\tilde{\mathcal{G}}$ that starts from $(p_{in}, \perp, (\emptyset, \dots, \emptyset), c(p_{in}))$, that ends with $(p, \alpha, \vec{R}, c)$ and where Eve respects $\tilde{\sigma}$.

3. c is the largest colour visited since α was pushed.

4. If $\pi$ is extended by some move that pops $\alpha$, the configuration $(r,s)$ that is reached is such that $r \in R_c$.

*Proof.* The proof goes by induction on $\pi$. We first show that the last point is a consequence of the second and third points. To aid readability, one can refer to Figure 10.3. Assume that the next move after (p, sα) is to apply a transition (r, pop) ∈ Δ(p, α). The second point implies that (p, α, $\vec{R}$, c) is winning for Eve in $\tilde{\mathcal{G}}$. If $p \in Q_{\text{Eve}}$, by definition of $\sigma$, there is some edge from that vertex to *t*, which means that $r \in R_c$ and allows us to conclude. If $p \in Q_{\text{Adam}}$, note that there is no edge from (p, α, $\vec{R}$, c) (winning position for Eve) to the (losing) vertex *ff*. Hence we conclude in the same way.

Let us now prove the other points. For this, assume that the result is proved for some play $\pi$, and let $\pi'$ be an extension of $\pi$. We have two cases, depending on how $\pi'$ extends $\pi$:

• $\pi'$ is obtained by applying a push transition. The result is trivial in that case.

• $\pi'$ is obtained by applying a pop transition. Let (p, sα) be the last configuration in $\pi$, and let $\vec{R}$ be the last vector component in $\text{top}(\Pi)$ when in configuration (p, sα). By the induction hypothesis, it follows that $\pi' = \pi \cdot (r,s)$ with $r \in R_c$. Considering how Π is updated, and using the fourth point, we easily deduce that the new strategy stack Π is as desired (one can have a look at Figure 10.3 for more intuition).
<figure><img src="image_82.png" /><figcaption>Figure 10.3: Updating the strategy's stack $\Pi$</figcaption></figure>
☐

Actually, we easily deduce a more precise result.

**Lemma 131.** Let $\pi$ be a finite play in $\mathcal{G}$ starting from $(p_{in}, \perp)$ and where Eve respects $\sigma$. Let $(\pi_i)_{i \ge 0}$ be its rounds factorisation. Let $\pi = \text{StCont}(\Pi)$, where $\Pi$ denotes the strategy's stack in the last vertex of $\pi$. Let $(\pi_i)_{i=0,\dots,k}$ be the rounds factorisation of $\pi$. Then the following holds:

* $\pi_i$ is a bump if and only if $\pi_i$ is a bump.

* $\pi_i$ has colour $c(\pi)_i$.

Both Lemma 130 and Lemma 131 are for finite plays. A version for infinite plays would allow us to conclude. Let $\pi$ be an infinite play in $\mathcal{G}$. We define an infinite version of $\pi$ by considering the limit of the stack contents $(\text{StCont}(\Pi_i))_{i \ge 0}$ where $\Pi_i$ is the strategy's stack after the first $i$ moves in $\pi$. It is easily seen that such a limit always exists, is infinite and corresponds to a play won by Eve in $\tilde{\mathcal{G}}$. Moreover the results of Lemma 131 apply.

Let $\pi$ be a play in $\mathcal{G}$ with initial vertex $(p_{in}, \perp)$, and where Eve respects $\sigma$, and let $\pi$ be the associated infinite play in $\tilde{\mathcal{G}}$. Therefore $\pi$ is won by Eve. Using Lemma 131 and Proposition 5, we conclude, as in the direct implication that $\pi$ is winning.

### 10.3.2 Solving the Game and Computing the Winning Region and Strategy

Combining Theorem 107 and Theorem 106, we obtain the following upper bounds regarding the problem of deciding the winner in a pushdown game and on constructing a finite state automaton recognising the winning region (in the sense of Remark 15).

**Theorem 108.** Let $\mathcal{G}$ be a parity pushdown game using colours $\{0, \dots, d-1\}$ and played on an arena generated by a pushdown system with $n$ control states and with a stack alphabet of size $m$. Then the following holds

(i) One can construct in time $\mathcal{O}(m^d 2^{nd^2})$ a deterministic finite state automaton with $2^n$ states recognising the winning region of Eve in $\mathcal{G}$.

(ii) One can decide in time $\mathcal{O}(m^d 2^{nd^2} + |s|)$, for any configuration $(p, \perp s)$, whether it is winning for Eve in $\mathcal{G}$.

*Proof.* Consider the parity game $\tilde{\mathcal{G}}$ from Section 10.3.1. Let $n = |Q|$ and $m = |\Gamma|$. Then $\tilde{\mathcal{G}}$ is played on an arena with $\mathcal{O}(nm 2^{2nd})$ vertices and it uses $d$ colours. Hence, computing the winning region of this later game can be achieved in time $\mathcal{O}(m^d 2^{nd^2})$, see Chapter 2.

Using, Theorem 107, it follows that the set of profiles can be computed in time $\mathcal{O}(m^d 2^{nd^2})$, and by Theorem 106 (and its proof) we know that we can construct (in the same time complexity) a deterministic finite state automaton with $2^n$ states recognising the winning region $W_{Eve}$.
The upper bound for the second item simply follows from the fact that running a
deterministic automaton on a word is performed in linear time in the length of the word.

☐

Regarding lower bound, the following result shows that the previous upper bound
is optimal. Note that it is enough to consider a reachability objective.

**Theorem 109.** Let $\mathcal{G}$ be a reachability pushdown game. Then the following problem is hard for EXP: decide whether $(p, \perp)$ is winning for Eve in $\mathcal{G}$.

*Proof.* The lower bound is established by reducing the halting problem for alternating
linear space bounded Turing machine.

Consider an alternating linear space bounded Turing machine $\mathcal{M}$. We can safely assume that $\mathcal{M}$ has a unique tape and on an input of size $n$ it uses at most $n$ tape squares. Let $Q = Q_\exists \cup Q_\forall$ be the states of the Turing machine where $Q_\exists$ are the existential states and $Q_\forall$ are the universal ones; we let $q_a$ be the (unique) accepting state of the machine. Call $A$ the tape alphabet and let $T \subseteq Q \times A \times Q \times A \times \{\leftarrow, \rightarrow\}$ the transition table of the machine. A configuration of $\mathcal{M}$ is a word $C$ of the form $uqv \in A^*QA^*$ of length $n+1$ (the meaning being that $\mathcal{M}$ is in state $q$ and that the tape contains $uv$).

We now informally describe a two-player game simulating a computation of $\mathcal{M}$
and argue that it can be encoded as a reachability pushdown game. Think first of $\mathcal{M}$
as being non-deterministic, i.e. $Q_\forall = \emptyset$ and call $C_0$ the initial configuration. A run
of $\mathcal{M}$ can be encoded as a word $r = C_0\#t_0\#C_1\#t_1\#C_2\#t_2\#C_3\#\dots$ where for every $i \ge 0$,
$t_i \in T$ is a transition of $\mathcal{M}$ that can be applied in configuration $C_i$ and $C_{i+1}$ is the
configuration reached from $C_i$ by applying $t_i$; it is accepting if some $t_i$ is a transition to
the accepting state of $\mathcal{M}$. A way to encode such $r$ with a pushdown game is that Eve
pushes symbols in the stack to describe $r$ and to use the control states to impose some
structural constraints on the sequence of pushed symbols:

* The first pushed configuration is $C_0$.

* Every configuration pushed has the right form, i.e. it is a word in $A^*QA^*$ of length $n+1$.

* Every configuration $C$ is followed by some pattern $\#t\#$ and the transition $t$ in this pattern can be applied from the configuration. This is ensured by storing in the control state of the pushdown process the state of $\mathcal{M}$ and the content of the currently read cell in $C$.

To ensure these properties a linear number of control states suffices.

Of course, this is not enough because Eve could cheat and push a configuration
$C_{i+1} = x_0x_1\cdots x_n$ which is not the successor of $C_i = y_0y_1\cdots y_n$ by $t_i$. To avoid this, after
she described a configuration (say $C_{i+1}$) and pushed the $\#$ symbol, Adam can stop the
simulation and claim a mistake by indicating the index $k$ of a wrong update in $C_{i+1}$. If
so, the game goes to a special mode where the following is performed:

* the $\#$ symbol is popped as well as the next $n-i$ symbols;

* the current top symbol is $x_i$ and it is stored in the control state of the pushdown
process
• the players keep popping until a `#` symbol is seen and the next symbol $t_i$ is also stored in the control state

• then the players pop $n-i-1$ symbols and then considering the next three symbols they can check whether the update was correct or not (there are several cases depending whether the reading tape was at distance at most 1 of the position of index $i$).

Again, this can be implemented thanks to a linear number of control states in the push-
down process.

In case Eve cheats the play loops in a non-final sink configuration. Otherwise it
loops in a final sink configuration.

Now, if the Turing Machine $\mathcal{M}$ is alternating, the only difference is that the choice of the transition $t_i$ is made by Eve if the control state in $C_i$ is existential and by Adam if it is universal. The rest of the game is unchanged (in particular Eve is still in charge of describing all configurations, regardless of whom picks the transition).

It is then immediate to check that Eve has a winning strategy in this game if and
only if the Turing machine accepts from its initial configuration. $\square$

**10.3.3 Pushdown and Regular Winning Strategies**

In Section 10.3.1, we have seen that the proof of Theorem 107 shows that a winning
strategy for Eve (when it exists) can be implemented by pushdown automaton that
reads the pushdown system transitions chosen by the players and indicates Eve moves
by a function depending only of the current control state and the top-most stack symbol
of the strategy automaton.

In this section, we present a different reduction whose aim is to be able to compute a
positional winning strategy for Eve which furthermore can be implemented by a finite
state automata. As an added benefit, we will see that this strategy is uniform in the
sense that it is winning from every vertex of the winning region of Eve.

For the rest of this section, we fix a parity pushdown game $\mathcal{G}$ played on an arena
$\mathcal{A} = (G, V_{\text{Eve}}, V_{\text{Adam}})$ generated by a pushdown system $\mathcal{P} = (Q, Q_{\text{Eve}}, Q_{\text{Adam}}, \Gamma, \Delta)$.
We also let $V = V_{\text{Eve}} \cup V_{\text{Adam}}$ and we let the colours used in the game be $\{0, \dots, d\}$.

A summary is a triple $(p, c, q) \in \mathcal{Q} \times \{0, \dots, d\} \times \mathcal{Q}$. A set $S$ of summaries is complete if $(p_1, c_1, q_1), (q, c_2, p_2) \in S$ implies that $(p_1, \max(c_1, c_2), p_2) \in S$; it is winning if $(p, c, p) \in S$ implies that $c$ is even. For $R \subseteq \mathcal{Q}$, a set of $R$-summaries is a set of summaries $S \subseteq R \times \{0, \dots, d\} \times R$. Associated with some stack content $s$, a summary $(p, c, q)$ aims to encode the existence of a sequence of moves from $(p, s)$ to $(q, s)$ where the top symbol of $s$ is never removed and where $c$ is the largest colour visited in the sequence.

Let $P \subseteq Q_{\text{Eve}}$ and $\gamma \in \Gamma_{\perp}$. A $(P, \gamma)$-local strategy for Eve is a partial function $\sigma_{\gamma}: P \to Q \times \{\text{pop, push}(\gamma) \mid \gamma \in \Gamma\}$ such that $\sigma_{\gamma}(p) \in \Delta(p, \gamma)$ for all $p \in P$. Equivalently it is a selection for every state in $P$ of a consistent transition of $\mathcal{P}$ when the top symbol is $\gamma$. For a subset $R \subseteq Q$, we say that $\sigma_{\gamma}$ pops in $R$ if $\sigma_{\gamma}(q) = (r, \text{pop})$ implies $r \in R$. We say that a $(P, \gamma)$-local strategy is safe if $\sigma_{\gamma}(p) = (q, \text{push}(\alpha))$ implies that $P \in \mathcal{R}(q, \alpha)$. From now on, we only allowed safe local strategies.
Let $R \subseteq Q$ and $\gamma \in \Gamma$. We associate with $(R, \gamma)$ the subset

$$W(R, \gamma) = \{q \mid R \in \mathcal{R}(q, \gamma)\}$$

By a small abuse of notation we let $W(\emptyset, \perp) = \{q \mid (q, \perp) \in W_{\text{Eve}}\}$. Remark that for every $q \in W(R, \gamma) \cap Q_{\text{Adam}}$ and $(r, \text{pop}) \in \Delta(q, \gamma)$ one has $r \in R$.

We now define a new game $\mathcal{G}$ played on a finite arena and equipped with an $\omega$-regular objective. We start by an informal description of plays in $\mathcal{G}$ and later formally describe the arena and the objective.

A play in $\mathcal{G}$ begins by an initialisation phase:

* The play starts in $(\perp, R)$ where $R = W(\emptyset, \perp) = \{q \mid (q, \perp) \in W_{\text{Eve}}\}$.

* From there, Eve chooses $\sigma_{\perp}$ an $(R, \perp)$-local strategy and a set of $R$-summaries that is both complete and winning. Then, the play goes to $(\perp, R, \sigma_{\perp}, S)$.

Then, the play goes for rounds of the following form:

* From a vertex $(\gamma, R, \sigma_{\gamma}, S)$, where $\gamma \in \Gamma$, $R \subseteq Q$, $\sigma_{\gamma}$ is an $(R, \gamma)$-local strategy and $S$ is a set of $R$-summaries, Eve chooses for every $\alpha \in \Gamma$ a $(W(R, \alpha), \alpha)$-local strategy $\sigma_{\alpha}$ that pops in $R$ and a set of $W(R, \alpha)$-summaries $S_{\alpha}$ that is both complete and winning. The play then goes in $(\gamma, R, \sigma_{\gamma}, S, (\sigma_{\alpha}, S_{\alpha})_{\alpha \in \Gamma})$.

* Then, Adam chooses some $\alpha$ in $\Gamma$ and the play goes in $(\alpha, W(R, \alpha), \sigma_{\alpha}, S_{\alpha})$.

Consider a tuple $(\gamma, R, \sigma_{\gamma}, S, (\sigma_{\alpha}, S_{\alpha})_{\alpha \in \Gamma})$ where $\gamma \in \Gamma$, $R \subseteq Q$, $\sigma_{\gamma}$ is an $(R, \gamma)$-local strategy, $S$ is a set of $R$-summaries, and, for every $\alpha \in \Gamma$, $\sigma_{\alpha}$ is a $(W(R, \alpha), \alpha)$-local strategy $\sigma_{\alpha}$ that pops in $R$ and $S_{\alpha}$ is a set of $W(R, \alpha)$-summaries that is both complete and winning. The tuple $(\gamma, R, \sigma_{\gamma}, (\sigma_{\alpha}, S_{\alpha})_{\alpha \in \Gamma})$ is consistent if, for every $(p, r) \in R^2$, one has $(p, \max(c(p), c, c(r)), r) \in S$ as soon as we are in one of the following two situations (the second one being the degenerated version of the first one).

* There exists $\alpha \in \Gamma$, $(q, c, q') \in S_{\alpha}$ such that

(i) either $p \in Q_{\text{Eve}}$ and $(q, \text{push}(\alpha)) = \sigma_{\gamma}(p)$, or $p \in Q_{\text{Adam}}$ and $(q, \text{push}(\alpha)) \in \Delta(p, \gamma)$, and

(ii) either $q' \in Q_{\text{Eve}}$ and $(r, \text{pop}) = \sigma_{\alpha}(q')$, or $q' \in Q_{\text{Adam}}$ and $(r, \text{pop}) \in \Delta(q', \alpha)$.

Intuitively, if with state $p$ and top symbol $\gamma$ one can push $\alpha$ and go to state $q$ from which we know that we can later go back to the same stack content with state $q'$ and maximal colour $c$, and finally pop $\gamma$ and end in state $r$, then we conclude that we can go from $p$ to $r$ while seeing $\max(c(p), c, c(r))$ as the maximal colour.

* There exists $\alpha \in \Gamma$ and $q \in W(R, \alpha)$ such that

(i) either $p \in Q_{\text{Eve}}$ and $(q, \text{push}(\alpha)) = \sigma_{\gamma}(p)$, or $p \in Q_{\text{Adam}}$ and $(q, \text{push}(\alpha)) \in \Delta(p, \gamma)$, and

(ii) either $q \in Q_{\text{Eve}}$ and $(r, \text{pop}) = \sigma_{\alpha}(q)$, or $q \in Q_{\text{Adam}}$ and $(r, \text{pop}) \in \Delta(q, \alpha)$,

(iii) $c = c(q)$.
Intuitively, if with state $p$ and top symbol $\gamma$ one can push $\alpha$ and go to state $q$ and directly pops $\gamma$ and end in state $r$, then we conclude that we can go from $p$ to $r$ while seeing $\max(c(p), c(q), c(r))$ as the maximal colour.

In the previous informal description, the only allowed choices for $(\sigma_\alpha, S_\alpha)_{\alpha \in \Gamma}$ are those that leads to consistent tuples. Formally, we define the arena $\mathcal{A}$ as follows:

* There is a special initial vertex $(\perp, W(\emptyset, \perp))$ controlled by Eve.

* For every $\gamma \in \Gamma_\perp$, every $R \subseteq Q$, every $(R, \gamma)$-local strategy $\sigma_\gamma$ and every set of $R$-summaries that is both complete and winning there is a vertex $(\gamma, R, \sigma_\gamma, S)$ controlled by Eve.

* There is a vertex $(\gamma, R, \sigma_\gamma, S, (\sigma_\alpha, S_\alpha)_{\alpha \in \Gamma})$ controlled by Adam for every consistent such tuple.

* From every vertex $(\gamma, R, \sigma_\gamma, S)$ there is an edge to every vertex of the form $(\gamma, R, \sigma_\gamma, S, (\sigma_\alpha, S_\alpha)_{\alpha \in \Gamma})$.

* From every vertex $(\gamma, R, \sigma_\gamma, S, (\sigma_\alpha, S_\alpha)_{\alpha \in \Gamma})$ there is an edge to $(\alpha, W(R, \alpha), \sigma_\alpha, S_\alpha)$ for every $\alpha \in \Gamma$.

Hence, a play in $\mathcal{G}$ from the initial vertex $(\gamma_0, R_0) = (\perp, W(\emptyset, \perp))$ is a sequence of vertices

$$ \hat{\pi} = (\perp, R_0)(\gamma_0, R_0, \sigma_0, S_0)(\gamma_0, R_0, \sigma_0, S_0, (\sigma_\alpha^1, S_\alpha^1)_{\alpha \in \Gamma})(\gamma_1, R_1, \sigma_1, S_1) \\ (\gamma_1, R_1, \sigma_1, S_1, (\sigma_\alpha^2, S_\alpha^2)_{\alpha \in \Gamma})(\gamma_2, R_2, \sigma_2, S_2) \dots $$

with $\sigma_i = \sigma_{\gamma_i}^i$ and $S_i = S_{\gamma_i}^i$ for every $i \ge 1$.

It is losing for Eve if there exists $(q_i)_{i \ge 0}$, $(p_i)_{i \ge 0} \in Q^N$ and $(c_i)_{i \ge 0} \in \{0, \dots, d\}^N$ such that $\limsup(c_i)_{i \ge 0}$ is odd and for every $i \ge 0$ one has

* $(q_i, c_i, p_i) \in S_i$; and

* either $p_i \in Q_{Eve}$ and $(q_{i+1}, \text{push}(\gamma_{i+1})) = \sigma_i(p_i, \gamma_i)$ or $p_i \in Q_{Adam}$ and $(q_{i+1}, \text{push}(\gamma_{i+1})) \in \Delta((p_i, \gamma_i))$.

Note that it is easily seen that the previous objective is an $\omega$-regular one.

We denote by $\mathcal{G}$ the previous game. The following result relies on the connection between $\mathcal{G}$ and the original pushdown game $\mathcal{G}$.

**Theorem 110.** *Eve has a finite memory winning strategy in $\mathcal{G}$ from $(\perp, W(\emptyset, \perp))$.*

*Proof.* As the game $\mathcal{G}$ is played on a finite arena and equipped with an $\omega$-regular objective, it suffices to prove that Eve has a winning strategy from $(\perp, W(\emptyset, \perp))$.

Consider a positional strategy $\sigma$ for Eve in $\mathcal{G}$ that is winning on the whole winning region $W_{Eve}$. Note that existence of positional winning strategies is ensure because $\mathcal{G}$ is a parity game.
Let $s \in \perp\Gamma^*$ be some stack content. We define a set of summaries $S_s^\sigma$ associated with $s$ (and $\sigma$) by letting

$$S_{\sigma}^{s} = \{(p, c, q) \mid \exists \pi = v_0 \cdots v_k \text{ with } k > 0, v_0 = (p, s), v_k = (q, s), \text{sh}(v_i) \ge \text{sh}(v_0) \\ \text{for all } 0 \le i \le k, \text{ and such that Eve respects } \sigma \text{ in } \pi \text{ and } c \text{ is the largest} \\ \text{colour visited in } \pi\}$$

and, for every $(p, c, q) \in S_{\sigma}^{s}$, we select a play $\pi_{(p,c,q)}^{s}$ that witnesses $(p, c, q) \in S_{\sigma}^{s}$.

Using $\sigma$ we define a strategy $\hat{\sigma}$ for Eve in $\mathcal{G}$ and we later argue that it is winning for her from $(\perp, W(\emptyset, \perp))$.

* At the beginning of the play in $(\perp, R)$ with $R = W(\emptyset, \perp)$, Eve moves to $(\perp, R, \sigma_{\perp}, S)$ where $\sigma_{\perp}(r) = \sigma((r, \perp))$ for every $r \in R$, and $S = S_{\sigma}^{\perp}$

* Assume the current play is

$$\hat{\pi} = (\perp, R_0)(\gamma_0, R_0, \sigma_0, S_0)(\gamma_0, R_0, \sigma_0, S_0, (\sigma_{\alpha}^1, S_{\alpha}^1)_{\alpha \in \Gamma})(\gamma_1, R_1, \sigma_1, S_1) \cdots (\gamma_k, R_k, \sigma_k, S_k)$$

and let $s_{\hat{\pi}} = \gamma_0 \cdots \gamma_k$. Then, Eve goes to $(\gamma_k, R_k, \sigma_k, S_k, (\sigma_{\alpha}^{k+1}, S_{\alpha}^{k+1})_{\alpha \in \Gamma}))$ with $\sigma_{\alpha}^{k+1}(r) = \sigma((r, s_{\hat{\pi}}\alpha))$ for every $r$ such that $(r, s_{\hat{\pi}}\alpha) \in W_{\text{Eve}}$ and $S_{\alpha}^{k+1} = S_{\sigma}^{\hat{\pi}\alpha}$.

Assume now by contradiction that $\hat{\sigma}$ is not winning and consider a losing play

$$\hat{\pi} = (\perp, R_0)(\gamma_0, R_0, \sigma_0, S_0)(\gamma_0, R_0, \sigma_0, S_0, (\sigma_{\alpha}^1, S_{\alpha}^1)_{\alpha \in \Gamma})(\gamma_1, R_1, \sigma_1, S_1) \\ (\gamma_1, R_1, \sigma_1, S_1, (\sigma_{\alpha}^2, S_{\alpha}^2)_{\alpha \in \Gamma})(\gamma_2, R_2, \sigma_2, S_2) \cdots$$

Hence, there exists $(q_i)_{i \ge 0}$, $(p_i)_{i \ge 0} \in \mathbb{Q}^N$ and $(c_i)_{i \ge 0} \in \{0, \dots, d\}^N$ such that $\limsup(c_i)_{i \ge 0}$ is odd and for every $i \ge 0$ one has

* $(q_i, c_i, p_i) \in S_i$; and

* either $p_i \in Q_{\text{Eve}}$ and $(q_{i+1}, \text{push}(\gamma_{i+1})) = \sigma_i(p_i, \gamma_i)$ or $p_i \in Q_{\text{Adam}}$ and $(q_{i+1}, \text{push}(\gamma_{i+1})) \in \Delta((p_i, \gamma_i))$.

Now, consider the play

$$\pi = \pi_{(q_0, c_0, p_0)}^{\gamma_0} \pi_{(q_1, c_1, p_1)}^{\gamma_0 \gamma_1} \pi_{(q_2, c_2, p_2)}^{\gamma_0 \gamma_1 \gamma_2} \pi_{(q_3, c_3, p_3)}^{\gamma_0 \gamma_1 \gamma_2 \gamma_3} \cdots$$

Then it is easily seen by definition that $\pi$ is losing (because $\hat{\pi}$ is) while Eve respects her winning strategy $\sigma$, which leads a contradiction and concludes the proof. $\square$

Following Theorem 110, fix a finite memory winning strategy $\hat{\sigma}$ for Eve in $\mathcal{G}$ from $(\perp, W(\emptyset, \perp))$. Using $\hat{\sigma}$ we define a positional strategy $\sigma$ for Eve in $\mathcal{G}$.

First, we inductively associate, with any word $s \in \perp\Gamma^*$, a finite play $\hat{\pi}_s$ in $\mathcal{G}$ where Eve respects her strategy $\hat{\sigma}$:

* If $s = \perp$, we let $\hat{\pi}_s = (\perp, W(\emptyset, \perp))(\perp, W(\emptyset, \perp), \sigma_{\perp}, S)$ where $(\perp, W(\emptyset, \perp), \sigma_{\perp}, S) = \hat{\sigma}((\perp, W(\emptyset, \perp)))$.
• If $s = s'\beta$ for some $\beta \in \Gamma$, let $\hat{\sigma}(\hat{\pi}_s') = (\gamma, R, \sigma_\gamma, S, (\sigma_\alpha, S_\alpha)_{\alpha \in \Gamma})$ and define

$$ \hat{\pi}_s = \hat{\pi}_{s'}(\gamma, R, \sigma_\gamma, S, (\sigma_\alpha, S_\alpha)_{\alpha \in \Gamma})(\beta, W(R, \beta), \sigma_\beta, S_\beta). $$

Now, for every configuration $(q, s)$ with $q \in Q_{Eve}$, we let $(\gamma, R, \sigma_\gamma, S_\gamma)$ be the last vertex in $\hat{\pi}_s$ and if $q \in R$ we let $\sigma((q, s)) = \sigma_\gamma(q)$ and otherwise we pick an arbitrary transition for $\sigma((q, s))$ as $(q, s)$ will be a losing position for Eve (see Proposition 8 below).

The following is a direct rephrasing of the proof of Theorem 106.

**Proposition 8.** Let $s \in \Gamma^* \perp$ and let $(\gamma, R, \sigma_\gamma, S)$ be the last vertex in $\hat{\pi}_s$. Then $R = \{p \mid (p, s) \in W_{Eve}\}$.

The following is a consequence of Proposition 8 and of the requirement that in a vertex $(\gamma, R, \sigma_\gamma, S)$ Eve should only propose $(W(R, \alpha), \alpha)$-local strategies that pops in $R$.

**Proposition 9.** Let $\pi$ be an infinite play in $\mathcal{G}$ starting from some winning position for Eve and where Eve respects strategy $\sigma$. Then any vertex visited in $\pi$ is a winning position for Eve.

*Proof.* It suffices to prove that the property is true for the second vertex in $\pi$ (and then conclude by induction as the strategy $\pi$ is positional). If the initial vertex belongs to Adam, then by definition all possible successors are winning for Eve (otherwise the initial one would be winning for Adam as well by prefix independence of the parity objective). If the initial vertex is controlled by Eve there are two cases depending whether her move is to push or pop a symbol. If the move is to pop a symbol then, by construction, the state reached belong to $R$ where the last vertex in $\hat{\pi}_s$ is $(\gamma, R, \sigma_\gamma, S)$, if $s$ denote the stack content after popping: hence, by Proposition 8 we conclude. If the move is to push a symbol then the result follows directly from the fact that we only consider safe local strategies and by Proposition 8. $\square$

The following is an easy consequence of the notion of consistent tuples.

**Proposition 10.** Let $(p, s) \in V$ and let $(\gamma, R, \sigma_\gamma, S)$ be the last vertex in $\hat{\pi}_s$. Assume that $p \in R$. Let $\pi = v_0 \cdots v_k$ be a finite play in $\mathcal{G}$ such that $k > 0$, $v_0 = (p, s)$, $\mathrm{sh}(v_i) \ge \mathrm{sh}(v_0)$ for every $0 < i < k$ and $v_k = (q, s)$ for some $q \in Q$. Then $(p, c, q) \in S$ where $c$ is the largest colour visited in $\pi$.

*Proof.* We do the proof only when we assume that the inequality $\mathrm{sh}(v_i) \ge \mathrm{sh}(v_0)$ is strict. The case where it is large is then a consequence of the fact that $S$ is complete with successive application of the strict case. The proof is by induction on $k$. The base case is when $k = 2$, and it corresponds to the degenerated case in the definition of consistent tuple. Now for the general case, when $k > 2$, one simply considers the play $v_1 \cdots v_{k-1}$, applies the induction hypothesis and conclude with the definition of consistent tuple again. $\square$

We are now ready to conclude and prove that $\sigma$ is a winning strategy for Eve.
**Theorem 111.** The positional strategy $\sigma$ is winning for Eve on the whole winning region in $\mathcal{G}$.

*Proof.* Consider an infinite play $\pi = v_0v_1\cdots$ starting from some winning position for Eve. Then by Proposition 9 we know that the play stays in the winning region.

By contradiction assume that $\pi$ is losing. We distinguish between two cases depending whether there is some vertex that is infinitely visited or not in $\pi$.

* Assume that there is a vertex $v = (q, s)$ that appears infinitely often in $\pi$ and choose one of minimal stack height. Let $k_0$ be such that $v_{k_0} = v$ and such that $\mathrm{sh}(v_j) \ge \mathrm{sh}(v)$ for every $j \ge k_0$. Let $(k_i)_{i \ge 0}$ be the increasing sequence of integers $k_i \ge k_0$ such that $v_{k_i} = v$. We claim that the largest colour visited in the segment $v_{k_i} \cdots v_{k_{i+1}}$ is even: indeed, it is a direct consequence of Proposition 10 and of the fact that the set of summaries we consider are winning. We then conclude that the largest colour infinitely visited in $\pi$ is even hence, leading a contradiction.

* Assume that no vertex is infinitely often visited in $\pi$. As the parity objective is prefix independent we can assume without loss of generality that there is no visited vertex with stack-height strictly smaller than $h = \mathrm{sh}(v_0)$. Factorise $\pi$ as $v_{i_0} \cdots v_{i_1-1}v_{i_1} \cdots v_{i_2-1}v_{i_2} \cdots v_{i_3-1} \cdots$ where $\mathrm{sh}(v_{i_j}) = \mathrm{sh}(v_{i_{j+1}-1}) = h+j$ and $\mathrm{sh}(v_k) > h+j$ for all $k \ge j+1$ (equivalently stack height $h+j$ is left forever in $v_{j+1}$). Call $s_j$ the stack content in $v_{i_j}$ and consider the infinite play $\hat{\pi}$ defined as the limit of the increasing (for prefix ordering) sequence of finite plays $(\hat{\pi}_{s_j})_{j \ge 0}$: it is a play in $\mathcal{G}$ where Eve respects $\hat{\sigma}$ hence, it is winning for her. Now let $v_{i_j} = (q_j, s_j)$, $v_{i_{j+1}-1} = (p_j, s_j)$ and let $c_j$ be the largest colour visited in $v_{i_j} \cdots v_{i_{j+1}-1}$. Then, as we assume that $\pi$ is losing one has $\limsup(c_i)_{i \ge 0}$ is odd. Moreover, if one lets

$$ \hat{\pi} = (\bot, R_0)(\gamma_0, R_0, \sigma_0, S_0)(\gamma_0, R_0, \sigma_0, S_0, (\sigma_\alpha^1, S_\alpha^1)_{\alpha \in \Gamma}))(\gamma_1, R_1, \sigma_1, S_1) \\ (\gamma_1, R_1, \sigma_1, S_1, (\sigma_\alpha^2, S_\alpha^2)_{\alpha \in \Gamma}))(\gamma_2, R_2, \sigma_2, S_2)\cdots $$

one has that

- $(q_i, c_i, p_i) \in S_i$ (by Proposition 10); and

- either $p_i \in Q_{\mathrm{Eve}}$ and $(q_{i+1}, \mathrm{push}(\gamma_{i+1})) = \sigma_i(p_i, \gamma_i)$ (by definition of $\sigma$) or $p_i \in Q_{\mathrm{Adam}}$ and $(q_{i+1}, \mathrm{push}(\gamma_{i+1})) \in \Delta((p_i, \gamma_i))$ (by definition of $\sigma$).

This means that $\hat{\pi}$ is losing, leading a contradiction.

Hence, we conclude that $\pi$ is winning which concludes the proof. $\square$

**Remark 18.** Note that the previous strategy $\sigma$ can be computed by a finite state automaton.

## Bibliographic references

The decidability of pushdown parity games is a consequence of the decidability of monadic second-order logic (MSO) on the infinite complete binary tree [Rab69b]. The
key observation is that any pushdown arena can be defined using MSO in the infinite complete binary tree $\Delta_2$. Indeed every node in $\Delta_2$ can be identified with the binary word encoding the path from the root to this node. Now, if one chooses a fixed-length encoding for the stack alphabet $\Gamma$ and for the set of states, a configuration $(p, s)$ can be associated to the node of $\Delta_2$ encoded by sp. Using this representation, the effect of a transition of the pushdown system can easily be captured by an MSO-formula. As a consequence, any property expressible in MSO on the arena can be effectively translated into equivalent MSO-property on the full binary tree.

This observation can be used to decide the winner of the game from any given vertex (i.e., Problem 1). It is indeed possible to write an MSO formula $\varphi_{\text{Eve}}(x)$ which expresses that Eve wins the games from $x$, see [Wal02] for parity games with possibly uncountable arenas. In the simpler case of pushdown arenas in which all vertices have a bounded outdegree writing such a formula is straightforward (see for instance [Cac03, Section 2.3.4]).

Rabin's lemma can be used to show that the winning regions are regular sets of configurations, as defined in Theorem 106. Recall that Rabin's lemma states that if the infinite tree $\Delta_2$ satisfies an existential MSO-formula $\exists X, \varphi(X)$ then there exists a regular set of nodes $R$ such that $\Delta_2$ satisfies $\varphi[R]$. Furthermore, a finite automaton accepting $R$ can be effectively constructed from $\varphi$. If we consider the formula $\varphi(X) = \forall x, x \in X \Leftrightarrow \varphi_{\text{Eve}}(x)$, we immediately obtain a finite automaton accepting the binary encodings of the configurations in the winning region for Eve. This automaton can easily be transformed to accept the configurations as in Theorem 106.

Using similar arguments, one can derive the existence of a regular positional winning strategy for both players in the sense of Section 10.3.3.

Although effective, these results do not provide tight upper-bounds as they rely on the translation of MSO properties into equivalent parity tree automata which is non-elementary in the alternation rank of the formula. In the sequel of this bibliographic note, we will focus on the history of decision procedures for pushdown games which provide explicit complexity bounds.

The first result on pushdown games can be traced back to the work of Büchi, which shows that the set of configurations reachable from the initial configuration of a pushdown system forms a regular language and hence can be represented by a finite state automaton [Büc64]. While Büchi's procedure is exponential, Caucal showed that this problem can be solved in polynomial time [Cau88]. The improved algorithm is a saturation process where transitions are incrementally added to a finite automaton. This technique was simplified and adapted to two-player reachability pushdown games where the target set is a regular set of configurations by Bouajjani et al. in [BEM97] and independently in [FWW97]. This saturation approach corresponds to the fixpoint characterization of strategy profiles in Section 10.2.1. This method was latter extended to Büchi pushdown games [Cac02] and finally to parity pushdown games [HO09]. We refer the reader to [CH14] for a survey of this method.

The decidability of parity pushdown games was established in [Wal01] where Walukiewicz gives algorithms to compute winning strategies for both players from a given configuration based on a deterministic pushdown automaton reading the moves of the play (as in Section 10.3.3). In this article, it is also shown that deciding the winner in a two-player pushdown reachability game is hard for EXP. In [Ser03, Cac02], the win-
ning region for both players was shown to be regular based on similar arguments as those presented in Section 10.2. The proof presented in this chapter follows [Ser04], except for the construction of a regular winning strategy given in Section 10.3.3 which is novel.

Kupferman and Vardi in [KV00] reduced deciding the winner in a parity push-
down game to the emptiness problem for two-way alternating parity tree automata. In
[Var98], Vardi had previously shown that this emptiness problem for this model of au-
tomata is in EXP. In addition, this approach permits to compute a finite automaton
accepting the winning region for both players, as well as regular winning strategies
for both players. The reduction is very close to the reduction to the decidability of
MSO on the full binary tree sketched in the beginning of this section, but by replacing
MSO-formulas with two-way alternating parity tree automata, one can obtain optimal
complexity (see [Cac02] for a survey of this approach). A similar approach was used
by Serre in [Ser06b] to study parity one-counter games (i.e. parity pushdown games
with a one-letter stack alphabet): by a reduction to the emptiness problem for two-way
alternating parity word automaton, one obtains a PSPACE upper bound (which is also
a matching lower bound).

They were many subsequent works on extensions of parity pushdown games. One
line of research considered non-regular winning conditions, based on properties of the
stack behaviour along the play [CDT02, BSW03, Gim04, Ser06a]. Another line of re-
search focused on considering games played on infinite arenas generated by extensions
of pushdown automata, mainly higher-order pushdown automata and collapsible push-
down automata, mostly motivated by connections with higher-order recursion schemes
(for further references on the topic we refer to [BCH<sup>+</sup>21, CS21]).
# GAMES WITH COUNTERS

<figure><img src="image_83.png" /></figure>
Chapter 11

# Games with Counters

SYLVAIN SCHMITZ

Just like timed games arise from timed systems and pushdown games from pushdown systems, counter games arise from (multi-)counter systems. Those are finite-state systems further endowed with a finite number of counters whose values range over the natural numbers, and are widely used to model and reason about systems handling discrete resources. Such resources include for instance money on a bank account, items on a factory line, molecules in chemical reactions, organisms in biological ones, replicated processes in distributed computing, etc. As with timed or pushdown systems, counter systems give rise to infinite graphs that can be turned into infinite game arenas.

One could populate a zoo with the many variants of counter systems, depending on the available counter operations. One of the best known specimens in this zoo are *Minsky machines* [Min67], where the operations are incrementing a counter, decrementing it, or testing whether its value is zero. Minsky machines are a universal model of computation: their reachability problem is undecidable, already with only two counters. From the algorithmic perspective we promote in this book, this means that the counter games arising from Minsky machines are not going to be very interesting, unless perhaps if we restrict ourselves to a single counter. A more promising species in our zoo are *vector addition systems with states* [Gre78, HP79]—or, equivalently, *Petri nets* [Pet62]—, where the only available operations are increments and decrements. Vector addition systems with states enjoy a decidable reachability problem [May81, Kos82, Lam92, Ler11], which makes them a much better candidate for studying the associated games.

In this chapter, we focus on vector games, that is, on games defined on arenas defined by vector addition systems with states with a partition of states controlled by Eve and Adam. As we are going to see in Section 11.1, those games turn out to be undecidable already for quite restricted objectives and just two counters. We then investigate two restricted classes of vector games.

1. In Section 11.2, we consider *one-counter games*. These can be reduced to the
pushdown games of Chapter 10 and are therefore decidable. Most of the section is thus devoted to proving sharp complexity lower bounds, already in the case of so-called *countdown games*.

2. In Section 11.3, we turn our attention to the main results of this chapter. By suitably restricting both the systems, with an *asymmetry* condition that forbids Adam to manipulate the counters, and the objective, with a *monotonicity* condition that ensures that Eve's winning region is upwards closed—meaning that larger counter values make it easier for her to win—, one obtains a class of decidable vector games where finite memory strategies are sufficient.

* This class is still rich enough to find many applications, and we zoom in on the connections with resource-conscious games like *energy games* and *bounding games* in Section 11.4—a subject that will be taken further in Chapter 12.

* The computational complexity of asymmetric monotonic vector games is now well-understood, and we devote Section 11.5 to the topic; Table 11.1 at the end of the chapter summarises these results.

## 11.1 Vector games

A *vector system* is a finite directed graph with a partition of the vertices and weighted edges. Formally, it is a tuple $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$ where $k \in \mathbb{N}$ is a dimension, $\mathcal{L}$ is a finite set of locations partitioned into the locations controlled by Eve and Adam, i.e., $\mathcal{L} = \mathcal{L}_{\text{Eve}} \uplus \mathcal{L}_{\text{Adam}}$, and $A \subseteq \mathcal{L} \times \mathbb{Z}^k \times \mathcal{L}$ is a finite set of weighted actions. We write $\ell \xrightarrow{\vec{u}} \ell'$ rather than $(\ell, \vec{u}, \ell')$ for actions in $A$. A *vector addition system with states* is a vector system where $\mathcal{L}_{\text{Adam}} = \emptyset$, i.e., it corresponds to the one-player case.

**Example 7 (vector system).** Figure 11.1 presents a vector system of dimension two with locations $\{\ell, \ell'\}$ where $\ell$ is controlled by Eve and $\ell'$ by Adam.

<figure><img src="image_84.png" /><figcaption>Figure 11.1: A vector system.</figcaption></figure>

The intuition behind a vector system is that it maintains $k$ counters $c_1, \dots, c_k$ as- signed to integer values. An action $\ell \xrightarrow{\vec{u}} \ell' \in A$ then updates each counter by adding the corresponding entry of $\vec{u}$, that is for all $1 \le j \le k$, the action performs the update $c_j := c_j + \vec{u}(j)$.

Before we proceed any further, let us fix some notations for vectors in $\mathbb{Z}^k$. We write '$\vec{0}$' for the *zero vector* with $\vec{0}(j) \stackrel{\text{def}}{=} 0$ for all $1 \le j \le k$. For all $1 \le j \le k$, we write '$\vec{e}_j$' for the *unit vector* with $\vec{e}_j(j) \stackrel{\text{def}}{=} 1$ and $\vec{e}_j(j') \stackrel{\text{def}}{=} 0$ for all $j' \ne j$. Addition
and comparison are defined componentwise, so that for instance $\vec{u} \le \vec{u}'$ if and only if for all $1 \le j \le k$, $\vec{u}(j) \le \vec{u}'(j)$. We write $w(\ell \xrightarrow{\vec{u}} \ell') \stackrel{\text{def}}{=} \vec{u}$ for the weight of an action and $w(\pi) \stackrel{\text{def}}{=} \sum_{1 \le j \le |\pi|} w(\pi_j)$ for the cumulative weight of a finite sequence of actions $\pi \in A^*$. For a vector $\vec{u} \in \mathbb{Z}^k$, we use its infinity norm $\|\vec{u}\| \stackrel{\text{def}}{=} \max_{1 \le j \le k} |\vec{u}(j)|$, hence $\|\vec{0}\| = 0$ and $\|\vec{e}_j\| = \| -\vec{e}_j\| = 1$, and we let $\|\ell \xrightarrow{\vec{u}} \ell'\| \stackrel{\text{def}}{=} \|w(\ell \xrightarrow{\vec{u}} \ell')\| = \|\vec{u}\|$ and $\|A\| \stackrel{\text{def}}{=} \max_{a \in A} \|w(a)\|$. Unless stated otherwise, we assume that all our vectors are represented in binary, hence $\|A\|$ may be exponential in the size of $\mathcal{V}$.

## 11.1.1 Arenas and Games

A vector system gives rise to an infinite graph $G_N \stackrel{\text{def}}{=} (V, E)$ over the set of vertices $V \stackrel{\text{def}}{=} (\mathcal{L} \times \mathbb{N}^k) \cup \{\perp\}$. The vertices of the graph are either configurations $\ell(\vec{v})$ consisting of a location $\ell \in \mathcal{L}$ and a vector of non-negative integers $\vec{v} \in \mathbb{N}^k$—such a vector represents a valuation of the counters $c_1, \dots, c_k$, or the sink $\perp$.

Consider an action in $a = (\ell \xrightarrow{\vec{u}} \ell')$ in $A$: we see it as a partial function $a: \mathcal{L} \times \mathbb{N}^k \to \mathcal{L} \times \mathbb{N}^k$ with domain $dom a \stackrel{\text{def}}{=} \{\ell(\vec{v}) \mid \vec{v} + \vec{u} \ge \vec{0}\}$ and image $a(\ell(\vec{v})) \stackrel{\text{def}}{=} \ell'(\vec{v} + \vec{u})$; let also $dom A \stackrel{\text{def}}{=} \cup_{a \in A} dom a$. This allows us to define the set $E$ of edges as a set of pairs

$$E \stackrel{\text{def}}{=} \{(\ell(\vec{v}), a(\ell(\vec{v}))) \mid a \in A \text{ and } \ell(\vec{v}) \in \text{dom } a\} \\ \cup \{(\ell(\vec{v}), \perp) \mid \ell(\vec{v}) \notin \text{dom } A\} \cup \{(\perp, \perp)\},$$

where $\text{In}((v, v')) \stackrel{\text{def}}{=} v$ and $\text{Out}((v, v')) \stackrel{\text{def}}{=} v'$ for all edges $(v, v') \in E$. There is therefore an edge $(v, v')$ between two configurations $v = \ell(\vec{v})$ and $v' = \ell'(\vec{v}')$ if there exists an action $\ell \xrightarrow{\vec{u}} \ell' \in A$ such that $\vec{v}' = \vec{v} + \vec{u}$. Note that, quite importantly, $\vec{v} + \vec{u}$ must be non-negative on every coordinate for this edge to exist. If no action can be applied, there is an edge to the sink $\perp$, which ensures that $E$ is total: for all $v \in V$, there exists an edge $(v, v') \in E$ for some $v'$, and thus there are no ‘deadlocks’ in the graph.

The configurations are naturally partitioned into those in $V_{\text{Eve}} \stackrel{\text{def}}{=} \mathcal{L}_{\text{Eve}} \times \mathbb{N}^k$ controlled by Eve and those in $V_{\text{Adam}} \stackrel{\text{def}}{=} \mathcal{L}_{\text{Adam}} \times \mathbb{N}^k$ controlled by Adam. Regarding the sink, the only edge starting from $\perp$ loops back to it, and it does not matter who of Eve or Adam controls it. This gives rise to an infinite arena $\mathcal{A}_N \stackrel{\text{def}}{=} (G_N, V_{\text{Eve}}, V_{\text{Adam}})$ called the natural semantics of $\mathcal{V}$.

Although we work in a turn-based setting with perfect information, it is sometimes enlightening to consider the partial map $\Delta: V \times A \to E$ defined by $\Delta(\ell(\vec{v}), a) \stackrel{\text{def}}{=} (\ell(\vec{v}), a(\ell(\vec{v})))$ if $\ell(\vec{v}) \in \text{dom } a$ and $\Delta(\ell(\vec{v}), a) \stackrel{\text{def}}{=} (\ell(\vec{v}), \perp)$ if $\ell(\vec{v}) \notin \text{dom } a$. Note that a sequence $\pi$ over $E$ that avoids the sink can also be described by an initial configuration $\ell_0(\vec{v}_0)$ paired with a sequence over $A$.

**Example 8 (natural semantics).** Figure 11.2 illustrates the natural semantics of the system of Figure 11.1; observe that all the configurations $\ell(0, n)$ for $n \in \mathbb{N}$ lead to the sink.

A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, a colouring $c: E \to C$, and an objective $\Omega \subseteq C^\omega$ together define a vector game $\mathcal{G} = (\mathcal{A}_N(\mathcal{V}), c, \Omega)$. Because $\mathcal{A}_N(\mathcal{V})$ is an infinite arena, we need to impose restrictions on our colourings $c: E \to C$ and the qualitative objectives $\Omega \subseteq C^\omega$; at the very least, they should be recursive.
<figure><img src="image_85.png" /><figcaption>Figure 11.2: The natural semantics of the vector system of Figure 11.1: a circle (resp. a square) at position $(i, j)$ of the grid denotes a configuration $\ell(i, j)$ (resp. $\ell'(i, j)$) controlled by Eve (resp. Adam).</figcaption></figure>

There are then two variants of the associated decision problem:

* the *given initial credit* variant, where we are given $\mathcal{V}$, $c$, $\Omega$, a location $\ell_0 \in \mathcal{L}$ and an initial credit $\vec{v}_0 \in \mathbb{N}^k$, and ask whether Eve wins $\mathcal{G}$ from the initial configuration $\ell_0(\vec{v}_0)$;

* the *existential initial credit* variant, where we are given $\mathcal{V}$, $c$, $\Omega$, and a location $\ell_0 \in \mathcal{L}$, and ask whether there exists an initial credit $\vec{v}_0 \in \mathbb{N}^k$ such that Eve wins $\mathcal{G}$ from the initial configuration $\ell_0(\vec{v}_0)$.

Let us instantiate the previous abstract definition of vector games. We first consider two 'reachability-like' objectives, where $C \stackrel{\text{def}}{=} \{\epsilon, \text{Win}\}$ and $\Omega \stackrel{\text{def}}{=} \text{Reach}$, namely configuration reachability and coverability. The difference between the two is that, in the configuration reachability problem, a specific configuration $\ell_f(\vec{v}_f)$ should be visited, whereas in the coverability problem, Eve attempts to visit $\ell_f(\vec{v}')$ for some vector $\vec{v}'$ componentwise larger or equal to $\vec{v}_f$.<fnref n="1" />

**Problem 13 (configuration reachability vector game with given initial credit).**

**INPUT:** A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, an initial location $\ell_0 \in \mathcal{L}$, an initial credit $\vec{v}_0 \in \mathbb{N}^k$, and a target configuration $\ell_f(\vec{v}_f) \in \mathcal{L} \times \mathbb{N}^k$.

**OUTPUT:** Does Eve have a strategy to reach $\ell(\vec{v})$ from $\ell_0(\vec{v}_0)$? That is, does she win the configuration reachability game $(\mathcal{A}_{\mathbb{N}(\mathcal{V})}, c, \text{Reach})$ from $\ell_0(\vec{v}_0)$, where $c(e) = \text{Win if and only if } \text{In}(e) = \ell_f(\vec{v}_f)$?

**Problem 14 (coverability vector game with given initial credit).**

**INPUT:** A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, an initial location $\ell_0 \in \mathcal{L}$, an initial credit $\vec{v}_0 \in \mathbb{N}^k$, and a target configuration $\ell_f(\vec{v}_f) \in \mathcal{L} \times \mathbb{N}^k$.

**OUTPUT:** Does Eve have a strategy to reach $\ell(\vec{v}')$ for some $\vec{v}' \ge \vec{v}_f$ from $\ell_0(\vec{v}_0)$? That is, does she win the coverability game $(\mathcal{A}_{\mathbb{N}(\mathcal{V})}, c, \text{Reach})$ from $\ell_0(\vec{v}_0)$, where $c(e) = \text{Win if and only if } \text{In}(e) = \ell_f(\vec{v}')$ for some $\vec{v}' \ge \vec{v}_f$?

<footnote n="1">¹The name 'coverability' comes from the the literature on Petri nets and vector addition systems with states, because Eve is attempting to cover $\ell_f(\vec{v}_f)$, i.e., to reach a configuration $\ell_f(\vec{v}')$ with $\vec{v}' \ge \vec{v}_f$.</footnote>
**Example 9 (Objectives).** Consider the target configuration $\ell(2,2)$ in Figures 11.1 and 11.2. Eve's winning region in the configuration reachability vector game is $W_{Eve} = \{\ell(n+1, n+1) | n \in \mathbb{N}\} \cup \{\ell'(0,1)\}$, displayed on the left in Figure 11.3. Eve has indeed an obvious winning strategy from any configuration $\ell(n,n)$ with $n \ge 2$, which is to use the action $\ell \xrightarrow{-1,-1} \ell$ until she reaches $\ell(2,2)$. Furthermore, in $\ell'(0,1)$—due to the natural semantics—, Adam has no choice but to use the action $\ell' \xrightarrow{2,1} \ell$: therefore $\ell'(0,1)$ and $\ell(1,1)$ are also winning for Eve.

<figure><img src="image_86.png" /><figcaption>Figure 11.3: The winning regions of Eve in the configuration reachability game (left) and the coverability game (right) on the graphs of Figures 11.1 and 11.2 with target configuration $\ell(2,2)$. The winning vertices are in filled in green, while the losing ones are filled with white with a red border; the sink is always losing.</figcaption></figure>

In the coverability vector game, Eve's winning region is $W_{Eve} = \{\ell(m+2, n+2), \ell'(m+2, n+2), \ell'(0, n+1), \ell(1, n+2), \ell'(2m+2, 1), \ell(2m+3, 1) | m, n \in \mathbb{N}\}$ displayed on the right in Figure 11.3. Observe in particular that Adam is forced to use the action $\ell' \xrightarrow{2,1} \ell$ from the configurations of the form $\ell'(0, n+1)$, which brings him to a configuration $\ell(2, n+2)$ coloured Win in the game, and thus the configurations of the form $\ell(1, n+1)$ are also winning for Eve since she can play $\ell \xrightarrow{-1,0} \ell'$. Thus the configurations of the form $\ell(2m+3, n+1)$ are also winning for Eve, as she can play the action $\ell \xrightarrow{-1,0} \ell'$ to a winning configuration $\ell'(2m+2, n+1)$ where all the actions available to Adam go into her winning region.

**Remark 19 (Location reachability).** One can notice that coverability is equivalent to location reachability, where we are given a target location $\ell_f$ but no target vector, and want to know whether Eve have a strategy to reach $\ell_f(\vec{v})$ for some $\vec{v}$.

Indeed, in both configuration reachability and coverability, we can assume without loss of generality that $\ell_f \in \mathcal{L}_{Eve}$ is controlled by Eve and that $\vec{v}_f = \vec{0}$ is the zero vector. Here is a LOGSPACE reduction to that case. If $\ell_0(\vec{v}_0) = \ell_f(\vec{v}_f)$ in the case of configuration reachability, or $\ell_0 = \ell_f$ and $\vec{v}_0 \ge \vec{v}_f$ in the case of coverability, the problem is trivial. Otherwise, any winning play must use at least one action. For each incoming action $a = (\ell \xrightarrow{\vec{u}} \ell_f)$ of $\ell_f$, create a new location $\ell_a$ controlled by Eve and replace a by $\ell \xrightarrow{\vec{u}} \ell_a \xrightarrow{0} \ell_f$, so that Eve gains the control right before any play reaches $\ell_f$. Also add a new location $\odot$ controlled by Eve with actions $\ell_a \xrightarrow{-\vec{v}_f} \odot$, and use $\odot(\vec{0})$ as target configuration.

**Remark 20 (Coverability to reachability).** There is a LOGSPACE reduction from coverability to configuration reachability. By Remark 19, we can assume without loss of generality that $\ell_f \in \mathcal{L}_{Eve}$ is controlled by Eve and that $\vec{v}_f = \vec{0}$ is the zero vector. It suffices therefore to add an action $\ell_f \xrightarrow{-e_i} \ell_f$ for all $1 \le j \le k$.
Departing from reachability games, the following is a very simple kind of safety
games where $C \stackrel{\text{def}}{=} \{\epsilon, \text{ Lose}\}$ and $\Omega \stackrel{\text{def}}{=} \text{ Safe}$; Figure 11.4 shows Eve's winning region
in the case of the graphs of Figures 11.1 and 11.2.

**Problem 15** (non-termination vector game with given initial credit).

**INPUT:** A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, an initial location $\ell_0 \in \mathcal{L}$, and an initial credit $\vec{v}_0 \in \mathbb{N}^k$.

**OUTPUT:** Does Eve have a strategy to avoid the sink $\perp$ from $\ell_0(\vec{v}_0)$? That is, does she win the non-termination game $(\mathcal{A}_N(\mathcal{V}), c, \text{Safe})$ from $\ell_0(\vec{v}_0)$, where $c(e) = \text{Lose}$ if and only if $\text{In}(e) = \perp$?

<figure><img src="image_87.png" /><figcaption>Figure 11.4: The winning region of Eve in the non-termination game on the graphs of Figures 11.1 and 11.2.</figcaption></figure>

Finally, one of the most general vector games are parity games, where $C \stackrel{\text{def}}{=} \{1, \dots, d\}$ and $\Omega \stackrel{\text{def}}{=} \text{Parity}$. In order to define a colouring of the natural semantics, we assume that we are provided with a *location colouring* lcol: $\mathcal{L} \to \{1, \dots, d\}$.

**Problem 16** (parity vector game with given initial credit).

**INPUT:** A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, an initial location $\ell_0 \in \mathcal{L}$, an initial credit $\vec{v}_0 \in \mathbb{N}^k$, and a location colouring lcol: $\mathcal{L} \to \{1, \dots, d\}$ for some $d > 0$.

**OUTPUT:** Does Eve have a strategy to simultaneously avoid the sink $\perp$ and fulfil the parity objective from $\ell_0(\vec{v}_0)$? That is, does she win the parity game $(\mathcal{A}_N(\mathcal{V}), c, \text{Parity})$ from $\ell_0(\vec{v}_0)$, where $c(e) \stackrel{\text{def}}{=} \text{lcol}(\ell)$ if $\text{In}(e) = \ell(\vec{v})$ for some $\vec{v} \in \mathbb{N}^k$, and $c(e) \stackrel{\text{def}}{=} 1$ if $\text{In}(e) = \perp$?

**Remark 21** (Non termination to parity). There is a LOGSPACE reduction from non-termination to parity. Indeed, the two games coincide if we pick the constant location colouring defined by $\text{lcol}(\ell) \stackrel{\text{def}}{=} 2$ for all $\ell \in \mathcal{L}$ in the parity game.

**Remark 22** (Coverability to parity). There is a LOGSPACE reduction from coverability to parity. Indeed, by Remark 19, we can assume that $\ell_f \in \mathcal{L}_{\text{Eve}}$ is controlled by Eve and that the target credit is $\vec{v}_f = \vec{0}$ the zero vector. It suffices therefore to add an action $\ell_f \xrightarrow{\vec{0}} \ell_f$ and to colour every location $\ell \neq \ell_f$ with $\text{lcol}(\ell) \stackrel{\text{def}}{=} 1$ and to set $\text{lcol}(\ell_f) \stackrel{\text{def}}{=} 2$.

The existential initial credit variants of Problems 13 to 16 are defined similarly,
where $\vec{v}_0$ is not given as part of the input, but existentially quantified in the question.
11.1.2 Undecidability

The bad news is that, although Problems 13 to 16 are all decidable in the one-player case—see the bibliographic notes Section 11.5.3 at the end of the chapter—, they become undecidable in the two-player setting.

**Theorem 112** (Undecidability of vector games). *Configuration reachability, coverability, non-termination, and parity vector games, both with given and with existential initial credit, are undecidable in any dimension* $k \ge 2$.

*Proof.* By Remarks 20 and 21, it suffices to prove the undecidability of coverability and non-termination. For this, we exhibit reductions from the halting problem of deterministic Minsky machines with at least two counters.

Formally, a *deterministic Minsky machine* with $k$ counters. $\mathcal{M} = (\mathcal{L}, A, k)$ is defined similarly to a vector addition system with states with additional *zero test actions* $a = (\ell \xrightarrow{i=0} \ell')$. The set of locations contains a distinguished 'halt' location $\ell_{\text{halt}}$, and for every $\ell \in \mathcal{L}$, exactly one of the following holds: either (i) $(\ell \xrightarrow{\vec{e}_i} \ell') \in A$ for some $0 < i \le k$ and $\ell' \in \mathcal{L}$, or (ii) $(\ell \xrightarrow{i=0} \ell') \in A$ and $(\ell \xrightarrow{-\vec{e}_i} \ell'') \in A$ for some $0 < i \le k$ and $\ell', \ell'' \in \mathcal{L}$, or (iii) $\ell = \ell_{\text{halt}}$. The semantics of $\mathcal{M}$ extends the natural semantics by handling zero tests actions $a = (\ell \xrightarrow{i=0} \ell')$: we define the domain as $\text{dom } a \stackrel{\text{def}}{=} \{\ell(\vec{v}) \mid \vec{v}(i) = 0\}$ and the image by $a(\ell(\vec{v})) \stackrel{\text{def}}{=} \ell(\vec{v})$. This semantics is deterministic, and from any starting vertex of $\mathcal{A}_{\mathbb{N}}(\mathcal{M})$, there is a unique play, which either eventually visits $\ell_{\text{halt}}$ and then the sink in the next step, or keeps avoiding both $\ell_{\text{halt}}$ and the sink indefinitely.

The *halting problem* asks, given a deterministic Minsky machine and an initial location $\ell_0$, whether it halts, that is, whether $\ell_{\text{halt}}(\vec{v})$ is reachable for some $\vec{v} \in \mathbb{N}^k$ starting from $\ell_0(\bar{0})$. The halting problem is undecidable in any dimension $k \ge 2$ [Min67]. Thus the halting problem is akin to the coverability of $\ell_{\text{halt}}(\bar{0})$ with given initial credit $\bar{0}$, but on the one hand there is only one player and on the other hand the machine can perform zero tests.

<figure><img src="image_88.png" /><figcaption>Figure 11.5: Schema of the reduction in the proof of Theorem 112.</figcaption></figure>

Here is now a reduction to Problem 14. Given an instance of the halting problem, i.e., given a deterministic Minsky machine $\mathcal{M} = (\mathcal{L}, A, k)$ and an initial location $\ell_0$, we construct a vector system $\mathcal{V} \stackrel{\text{def}}{=} (\mathcal{L} \uplus \mathcal{L}_{\bar{0}} \uplus \{\otimes\}, A', \mathcal{L}, \mathcal{L}_{\bar{0}} \uplus \{\otimes\}, k)$ where all the original locations are controlled by Eve and $\mathcal{L}_{\bar{0}} \uplus \{\otimes\}$ is a set of new locations
controlled by Adam. We use $\mathcal{L}_{\underline{0}}$ as a set of locations defined by

$$ \mathcal{L}_{\underline{0}}^{\text{def}} = \{ \ell'_{i \underline{0}} | \exists \ell \in \mathcal{L} . (\ell \xrightarrow{i \underline{0}} \ell') \in A \} $$

and define the set of actions by (see Figure 11.5)

$$ A' \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \{ \ell \xrightarrow{\vec{e}_i} \ell' | (\ell \xrightarrow{\vec{e}_i} \ell') \in A \} \cup \{ \ell \xrightarrow{-\vec{e}_i} \ell'' | (\ell \xrightarrow{\vec{e}_i} \ell'') \in A \} \\ \cup \{ \ell \xrightarrow{\vec{0}} \ell'_{i \underline{0}}, \ell'_{i \underline{0}} \xrightarrow{\vec{0}} \ell', \ell'_{i \underline{0}} \xrightarrow{-\vec{e}_i} \otimes | (\ell \xrightarrow{i \underline{0}} \ell') \in A \} \end{array} \right\}. $$

We use $\ell_0(\vec{0})$ as initial configuration and $\ell_{\text{halt}}(\vec{0})$ as target configuration for the constructed coverability instance. Here is the crux of the argument why Eve has a winning strategy to cover $\ell_{\text{halt}}(\vec{0})$ from $\ell_0(\vec{0})$ if and only if the Minsky machine halts. Consider any configuration $\ell(\vec{v})$. If $(\ell \xrightarrow{\vec{e}_i} \ell') \in A$, Eve has no choice but to apply $\ell \xrightarrow{\vec{e}_i} \ell'$ and go to the configuration $\ell'(\vec{v} + \vec{e}_i)$ also reached in one step in $\mathcal{M}$. If $\{\ell \xrightarrow{i \underline{0}} \ell', \ell \xrightarrow{-\vec{e}_i} \ell''\} \in A$ and $\vec{v}(i) = 0$, due to the natural semantics, Eve cannot use the action $\ell \xrightarrow{-\vec{e}_i} \ell''$, thus she must use $\ell \xrightarrow{\vec{0}} \ell'_{i \underline{0}}$. Still due to the natural semantics, Adam cannot use $\ell'_{i \underline{0}} \xrightarrow{-\vec{e}_i} \otimes$, thus he must use $\ell'_{i \underline{0}} \xrightarrow{\vec{0}} \ell'$. Hence Eve regains the control in $\ell'(\vec{v})$, which was also the configuration reached in one step in $\mathcal{M}$. Finally, if $\{\ell \xrightarrow{i \underline{0}} \ell', \ell \xrightarrow{-\vec{e}_i} \ell''\} \in A$ and $\vec{v}(i) > 0$, Eve can choose: if she uses $\ell \xrightarrow{-\vec{e}_i} \ell''$, she ends in the configuration $\ell''(\vec{v} - \vec{e}_i)$ also reached in one step in $\mathcal{M}$. In fact, she should not use $\ell \xrightarrow{\vec{0}} \ell'_{i \underline{0}}$, because Adam would then have the opportunity to apply $\ell'_{i \underline{0}} \xrightarrow{-\vec{e}_i} \otimes$ and to win, as $\otimes$ is a deadlock location and all the subsequent moves end in the sink. Thus, if $\mathcal{M}$ halts, then Eve has a winning strategy that simply follows the unique play of $\mathcal{M}$, and conversely, if Eve wins, then necessarily she had to follow the play of $\mathcal{M}$ and thus the machine halts.

Further note that, in a deterministic Minsky machine the halting problem is similarly akin to the complement of non-termination with given initial credit $\vec{0}$. This means that, in the vector system $\mathcal{V} = (\mathcal{L} \uplus \mathcal{L}_{\underline{0}} \uplus \{\otimes\}, A', \mathcal{L}, \mathcal{L}_{\underline{0}} \uplus \{\otimes\}, k)$ defined earlier, Eve has a winning strategy to avoid the sink from $\ell_0(\vec{0})$ if and only if the given Minsky machine does not halt from $\ell_0(\vec{0})$, which shows the undecidability of Problem 15.

Finally, let us observe that both the existential and the universal initial credit variants of the halting problem are also undecidable. Indeed, given an instance of the halting problem, i.e., given a deterministic Minsky machine $\mathcal{M} = (\mathcal{L}, A, k)$ and an initial location $\ell_0$, we add $k$ new locations $\ell_k, \ell_{k-1}, \dots, \ell_1$ with respective actions $\ell_j \xrightarrow{-\vec{e}_j} \ell_{j+1}$ and $\ell_j \xrightarrow{\vec{j}} \ell_{j+1}$ for all $k \ge j > 0$. This modified machine first resets all its counters to zero before reaching $\ell_0(\vec{0})$ and then performs the same execution as the original machine. Thus there exists an initial credit $\vec{v}$ such that the modified machine reaches $\ell_{\text{halt}}$ from $\ell_k(\vec{v})$ if and only if for all initial credits $\vec{v}$ the modified machine reaches $\ell_{\text{halt}}$ from $\ell_k(\vec{v})$, if and only if $\ell_{\text{halt}}$ was reachable from $\ell_0(\vec{0})$ in the original machine. The previous construction of a vector system applied to the modified machine then shows the undecidability of the existential initial credit variants of Problems 14 and 15. $\square$
## 11.2 Games in dimension one

Theorem 112 leaves open whether vector games might be decidable in dimension one. They are indeed decidable, and more generally we learned in Chapter 10 that one-counter games—with the additional ability to test the counter for zero—were decidable and in fact PSPACE-complete. This might seem to settle the case of vector games in dimension one, except that the one-counter games of Chapter 10 only allow integer weights in $\{-1, 1\}$, whereas we allow arbitrary updates in $\mathbb{Z}$ with a binary encoding. Hence the PSPACE upper bound of Chapter 10 becomes an EXPSPACE one for succinct one-counter games.

**Corollary 20** (One-dimensional vector games are in EXPSPACE). *Configuration reachability, coverability, non-termination, and parity vector games, both with given and with existential initial credit, are in EXPSPACE in dimension one.*

The goal of this section is therefore to establish that this EXPSPACE upper bound is tight (in most cases), by proving a matching lower bound in Section 11.2.2. But first, we will study a class of one-dimensional vector games of independent interest in Section 11.2.1: countdown games.

### 11.2.1 Countdown Games

A one-dimensional vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, 1)$ is called a *countdown system* if $A \subseteq \mathcal{L} \times \mathbb{Z}_{<0} \times \mathcal{L}$, that is, if for all $(\ell \xrightarrow{\mathbb{Z}} \ell') \in A$, $z < 0$. We consider the games defined by countdown systems, both with given and with existential initial credit, and call the resulting games *countdown games*.

**Theorem 113** (Countdown games are EXP-complete). *Configuration reachability and coverability countdown games with given initial credit are EXP-complete.*

*Proof.* For the upper bound, consider an instance, i.e., a countdown system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, 1)$, an initial location $\ell_0 \in \mathcal{L}$, an initial credit $n_0 \in \mathbb{N}$, and a target configuration $\ell_f(n_f) \in \mathcal{L} \times \mathbb{N}$. Because every action decreases strictly the counter value, the reachable part of the natural semantics of $\mathcal{V}$ starting from $\ell_0(n_0)$ is finite and of size at most $1 + |\mathcal{L}| \cdot (n_0 + 1)$, and because $n_0$ is encoded in binary, this is at most exponential in the size of the instance. As seen in Chapter 2, such a reachability game can be solved in time polynomial in the size of the finite graph, thus in EXP overall.

For the lower bound, we start by considering a game played over an exponential-time Turing machine, before showing how to implement this game as a countdown game. Let us consider for this an arbitrary Turing machine $M$ working in deterministic exponential time $2^{p(n)}$ for some fixed polynomial $p$ and an input word $w = a_1 \cdots a_n$ of length $n$, which we assume to be positive. Let $m \stackrel{\text{def}}{=} 2^{p(n)} \ge n$. The computation of $M$ on $w$ is a sequence of configurations $C_1, C_2, \ldots, C_t$ of length $t \le m$. Each configuration $C_i$ is of the form $\triangleright \gamma_{i,1} \cdots \gamma_{i,m} \triangleleft$ where $\triangleright$ and $\triangleleft$ are endmarkers and the symbols $\gamma_{i,j}$ are either taken from the finite tape alphabet $\Gamma$ (which includes a blank symbol $\Box$) or a pair $(q, a)$ of a state from $Q$ and a tape symbol $a$. We assume that the set of states $Q$
<table><caption>Figure 11.6: The computation of $\mathcal{M}$ on input $w = a_1 \cdots a_n$. This particular picture assumes $\mathcal{M}$ starts by rewriting $a_1$ into $a'_1$ and moving to the right in a state $q_1$, and empties its tape before accepting its input by going to state $q_{final}$.</caption><thead><tr><th></th><th>0</th><th>1</th><th>2</th><th>3</th><th>...</th><th>j-1</th><th>j</th><th>j+1</th><th>...</th><th>m</th><th>m+1</th></tr></thead><tbody><tr><td>C<sub>t</sub></td><td>▷</td><td>q<sub>final</sub>, □</td><td>□</td><td>□</td><td>...</td><td>□</td><td>□</td><td>□</td><td>...</td><td>□</td><td>▷</td></tr><tr><td>⋮</td><td></td><td></td><td></td><td></td><td></td><td>⋮</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>C<sub>i</sub></td><td>▷</td><td></td><td></td><td></td><td></td><td>...</td><td>γ<sub>i,j</sub></td><td>...</td><td></td><td></td><td>▷</td></tr><tr><td>C<sub>i-1</sub></td><td>▷</td><td></td><td></td><td></td><td></td><td>...</td><td>γ<sub>i-1,j-1</sub></td><td>γ<sub>i-1,j</sub></td><td>γ<sub>i-1,j+1</sub></td><td>...</td><td>▷</td></tr><tr><td>⋮</td><td></td><td></td><td></td><td></td><td></td><td>⋮</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>C<sub>2</sub></td><td>▷</td><td>a'<sub>1</sub></td><td>q<sub>1</sub>, a<sub>2</sub></td><td>a<sub>3</sub></td><td>...</td><td>□</td><td>□</td><td>□</td><td>...</td><td>□</td><td>▷</td></tr><tr><td>C<sub>1</sub></td><td>▷</td><td>q<sub>0</sub>, a<sub>1</sub></td><td>a<sub>2</sub></td><td>a<sub>3</sub></td><td>...</td><td>□</td><td>□</td><td>□</td><td>...</td><td>□</td><td>▷</td></tr></tbody></table>

contains a single accepting state $q_{final}$. The entire computation can be arranged over a $t \times m$ grid where each line corresponds to a configuration $C_i$, as shown in Figure 11.6.

We now set up a two-player game where Eve wants to prove that the input $w$ is accepted. Let $\Gamma' \stackrel{\text{def}}{=} \{\Delta, \Delta\} \cup \Gamma \cup (Q \times \Gamma)$. Rather than exhibiting the full computation from Figure 11.6, the game will be played over positions $(i, j, \gamma_{i,j})$ where $0 < i \le m$, $0 \le j \le m+1$, and $\gamma_{i,j} \in \Gamma'$. Eve wants to show that, in the computation of $\mathcal{M}$ over $w$ as depicted in Figure 11.6, the $j$th cell of the $i$th configuration $C_i$ contains $\gamma_{i,j}$. In order to substantiate this claim, observe that the content of any cell $\gamma_{i,j}$ in the grid is determined by the actions of $\mathcal{M}$ and the contents of (up to) three cells in the previous configuration. Thus, if $i > 1$ and $0 < j < m+1$, Eve provides a triple $(\gamma_{i-1,j-1}, \gamma_{i-1,j}, \gamma_{i-1,j+1})$ of symbols in $\Gamma'$ that yield $\gamma_{i,j}$ according to the actions of $\mathcal{M}$, which we denote by $\gamma_{i-1,j-1}, \gamma_{i-1,j}, \gamma_{i-1,j+1} \vdash \gamma_{i,j}$, and Adam chooses $j' \in \{j-1, j, j+1\}$ and returns the control to Eve in position $(i-1, j', \gamma_{i-1,j'})$. Regarding the boundary cases where $i=0$ or $j=0$ or $j=m+1$, Eve wins immediately if $j=0$ and $\gamma=\Delta$, or if $j=m+1$ and $\gamma=\Delta$, or if $i=0$ and $0 < j \le n$ and $\gamma=a_j$, or if $i=0$ and $n < j \le m$ and $\gamma=\square$, and otherwise Adam wins immediately. The game starts in a position $(t, j, (q_{final}, a))$ for some $0 < t \le m$, $0 < j \le m$, and $a \in \Gamma$ of Eve's choosing. It should be clear that Eve has a winning strategy in this game if and only if $w$ is accepted by $\mathcal{M}$.

We now implement the previous game as a coverability game over a countdown system $\mathcal{V} \stackrel{\text{def}}{=} (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, 1)$. The idea is that the pair $(i, j)$ will be encoded as $(i-1) \cdot (m+2) + j + 2$ in the counter value, while the symbol $\gamma_{i,j}$ will be encoded in the location. For instance, the endmarker $\Delta$ at position $(1, 0)$ will be represented by configuration $\ell_{\Delta}(2)$, the first input $(q_0, a_1)$ at position $(1, 1)$ by $\ell_{(q_0, a_1)}(3)$, and the endmarker $\Delta$ at position $(m, m+1)$ by $\ell_{\Delta}(m \cdot (m+2) + 1)$. The game starts from the initial configuration $\ell_0(n_0)$ where $n_0 \stackrel{\text{def}}{=} m \cdot (m+2) + 1$ and the target location is $\ominus$.
We define for this the sets of locations

$$
\begin{align*}
\mathcal{L}_{\text{Eve}} &\stackrel{\text{def}}{=} \{\ell_0, \odot, \oplus\} \cup \{\ell_{\gamma} \mid \gamma \in \Gamma'\}, \\
\mathcal{L}_{\text{Adam}} &\stackrel{\text{def}}{=} \{\ell_{(\gamma_1, \gamma_2, \gamma_3)} \mid \gamma_1, \gamma_2, \gamma_3 \in \Gamma'\} \cup \{\ell_{=j} \mid 0 < j \le n\} \cup \{\ell_{1 \le ? \le m-n+1}\}.
\end{align*}
$$

The intention behind the locations $\ell_j \in \mathcal{L}_{\text{Adam}}$ is that Eve can reach $\odot$ from a configuration $\ell_j(c)$ if and only if $c = j$; we accordingly define $A$ with the following actions, where $\odot$ is a deadlock location:

$$
\ell_j \xrightarrow{-j-1} \odot, \qquad \ell_j \xrightarrow{-j} \odot.
$$

Similarly, Eve should be able to reach $\odot$ from $\ell_{1\le ? \le m-n+1}(c)$ if and only if $1 \le c \le m-n+1$, which is implemented by the actions

$$
\ell_{1 \le ? \le m-n+1} \xrightarrow{-m+n-2} \odot, \quad \ell_{1 \le ? \le m-n+1} \xrightarrow{-1} \odot, \quad \odot \xrightarrow{-1} \odot.
$$

Note this last action also ensures that Eve can reach the location $\odot$ if and only if she can reach the configuration $\odot(0)$, thus the game can equivalently be seen as a configuration reachability game.

Regarding initialisation, Eve can choose her initial position, which we implement
by the actions

$$
\ell_0 \xrightarrow{-1} \ell_0 \qquad \ell_0 \xrightarrow{-1} \ell_{(q_{\text{final}}, a)} \qquad \text{for } a \in \Gamma.
$$

Outside the boundary cases, the game is implemented by the following actions:

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\ell_{\gamma} \xrightarrow{-m} \ell_{(\gamma_1, \gamma_2, \gamma_3)} & \text{for } \gamma_1, \gamma_2, \gamma_3 \vdash \gamma, & \\
\ell_{(\gamma_1, \gamma_2, \gamma_3)} \xrightarrow{-k} \ell_{\gamma_k} & \text{for } k \in \{1, 2, 3\}. &
\end{array}
$$

We handle the endmarker positions via the following actions, where Eve proceeds
along the left edge of Figure 11.6 until she reaches the initial left endmarker:

$$
\ell_{\triangleright} \xrightarrow{-m-2} \ell_{\triangleleft}, \quad \ell_{\triangleleft} \xrightarrow{-1} \ell_{=1}, \quad \ell_{\triangleleft} \xrightarrow{-m-1} \ell_{\triangleright}.
$$

For the positions inside the input word $w = a_1 \cdots a_n$, we use the actions

$$
\ell_{(q_0, a_1)} \xrightarrow{-2} \ell_{=1}, \qquad \ell_{aj} \xrightarrow{-2} \ell_{=j} \quad \text{for } 1 < j \le n.
$$

Finally, for the blank symbols of $C_1$, which should be associated with a counter value $c$ such that $n+3 \le c \le m+3$, we use the action

$$
\ell_{\square} \xrightarrow{-n-2} \ell_{1 \le ? \le m-n+1} .
$$

□

**Theorem 114** (Existential countdown games are EXPSPACE-complete). *Configuration reachability and coverability countdown games with existential initial credit are EXPSPACE-complete.*
*Proof.* For the upper bound, consider an instance, i.e., a countdown system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, 1)$, an initial location $\ell_0$, and a target configuration $\ell_f \in \mathcal{L}$. We reduce this to an instance of configuration reachability with given initial credit in a one-dimensional vector system by adding a new location $\ell'_0$ controlled by Eve with actions $\ell'_0 \xrightarrow{1} \ell'_0$ and $\ell'_0 \xrightarrow{0} \ell_0$, and asking whether Eve has a winning strategy starting from $\ell'_0(0)$ in the new system. By Corollary 20, this configuration reachability game can be solved in EXPSPACE.

For the lower bound, we reduce from the acceptance problem of a deterministic Turing machine working in exponential space. The reduction is the same as in the proof of Theorem 113, except that now the length $t$ of the computation is not bounded a priori, but this is compensated by the fact that we are playing the existential initial credit version of the countdown game. $\square$

Originally, countdown games were introduced with a slightly different objective, which corresponds to the following decision problem.

**Problem 17 (zero reachability with given initial credit).**

**INPUT:** A countdown system $\mathcal{V} = (\mathcal{L}, T, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, 1)$, an initial location $\ell_0 \in \mathcal{L}$, and an initial credit $n_0 \in \mathbb{N}$.

**OUTPUT:** Does Eve have a strategy to reach a configuration $\ell(0)$ for some $\ell \in \mathcal{L}$? That is, does she win the zero reachability game $(\mathcal{A}_N(\mathcal{V}), c, \mathit{Reach})$ from $\ell_0(n_0)$, where $c(e) = \mathit{Win}$ if and only if $\mathit{In}(e) = \ell(0)$ for some $\ell \in \mathcal{L}$?

**Theorem 115 (Countdown to zero games are EXP-complete).** Zero reachability count-down games with given initial credit are EXP-complete.

*Proof.* The upper bound of Theorem 113 applies in the same way. Regarding the lower bound, we modify the lower bound construction of Theorem 113 in the following way: we use $\ell_0(2 \cdot n_0 + 1)$ as initial configuration, multiply all the action weights in $A$ by two, and add a new location $\ell_{\mathit{zero}}$ with an action $\odot \xrightarrow{-1} \ell_{\mathit{zero}}$. Because all the counter values in the new game are odd unless we reach $\ell_{\mathit{zero}}$, the only way for Eve to bring the counter to zero in this new game is to first reach $\odot(1)$, which occurs if and only if she could reach $\odot(0)$ in the original game. $\square$

### 11.2.2 Vector Games in Dimension One

Countdown games are frequently employed to prove complexity lower bounds. Here, we use them to show that the EXPSPACE upper bounds from Corollary 20 are tight in most cases.

**Theorem 116 (The complexity of vector games in dimension one).** *Configuration reachability, coverability, and parity vector games, both with given and with existential initial credit, are EXPSPACE-complete in dimension one; non-termination vector games in dimension one are EXP-hard with given initial credit and EXPSPACE-complete with existential initial credit.*
*Proof.* By Theorem 114, configuration reachability and coverability vector games with existential initial credit are EXPSPACE-hard in dimension one. Furthermore, Remark 22 allows to deduce that parity is also EXPSPACE-hard. Finally, we can argue as in the upper bound proof of Theorem 114 that all these games are also hard with given initial credit: we add a new initial location $\ell'_0$ controlled by Eve with actions $\ell'_0 \xrightarrow{1} \ell'_0$ and $\ell'_0 \xrightarrow{0} \ell'_0$ and play the game starting from $\ell'_0(0)$.

Regarding non-termination, we can add a self loop $\odot \xrightarrow{0} \odot$ to the construction of Theorems 113 and 114: then the only way to build an infinite play that avoids the sink is to reach the target location $\odot$. This shows that the games are EXP-hard with given initial credit and EXPSPACE-hard with existential initial credit. Note that the trick of reducing existential to given initial credit with an initial incrementing loop $\ell'_0 \xrightarrow{1} \ell'_0$ does not work, because Eve would have a trivial winning strategy that consists in just playing this loop forever. $\square$

## 11.3 Asymmetric games

Theorem 112 shows that vector games are too powerful to be algorithmically relevant, except in dimension one where Theorem 116 applies. This prompts the study of restricted kinds of vector games, which might be decidable in arbitrary dimension. This section introduces one such restriction, called asymmetry, which turns out to be very fruitful: it yields decidable games (see Section 11.5), and is related to another class of games on counter systems called energy games (see Section 11.4).

**Asymmetric Games** A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, k)$ is asymmetric if, for all locations $\ell \in \mathcal{L}_{Adam}$ controlled by Adam and all actions $(\ell \xrightarrow{u} \ell') \in A$ originating from those, $\bar{u} = \bar{0}$ the zero vector. In other words, Adam may only change the current location, and cannot interact directly with the counters.

**Example 10** (Asymmetric vector system). Figure 11.7 presents an asymmetric vector system of dimension two with locations partitioned as $\mathcal{L}_{Eve} = \{\ell, \ell_{2,1}, \ell_{-1,0}\}$ and $\mathcal{L}_{Adam} = \{\ell'\}$. We omit the labels on the actions originating from Adam's locations, since those are necessarily the zero vector. It is worth observing that this vector system behaves quite differently from the one of Example 7 on p. 356: for instance, in $\ell'(0,1)$, Adam can now ensure that the sink will be reached by playing the action $\ell' \xrightarrow{0,0} \ell_{-1,0}$, whereas in Example 7, the action $\ell' \xrightarrow{-1,0} \ell$ was just inhibited by the natural semantics.

### 11.3.1 The Case of Configuration Reachability

In spite of the restriction to asymmetric vector systems, configuration reachability remains undecidable.

**Theorem 117** (Reachability in asymmetric vector games is undecidable). *Configuration reachability asymmetric vector games, both with given and with existential initial credit, are undecidable in any dimension $k \ge 2$.*
<figure><img src="image_89.png" /><figcaption>Figure 11.7: An asymmetric vector system.</figcaption></figure>

*Proof.* We first reduce from the halting problem of deterministic Minsky machines to configuration reachability with given initial credit. Given an instance of the halting problem, i.e., given $\mathcal{M} = (\mathcal{L}, A, k)$ and an initial location $\ell_0$ where we assume without loss of generality that $\mathcal{M}$ checks that all its counters are zero before going to $\ell_{halt}$, we construct an asymmetric vector system $\mathcal{V} \stackrel{\text{def}}{=} (\mathcal{L} \uplus \mathcal{L}_{\ge 0} \uplus \mathcal{L}_k, A', \mathcal{L} \uplus \mathcal{L}_{\ge 0}', \mathcal{L}_{\ge 0}, k)$ where all the original locations and $\mathcal{L}_k$ are controlled by Eve and $\mathcal{L}_{\ge 0}$ is controlled by Adam.

<figure><img src="image_90.png" /><figcaption>Figure 11.8: Schema of the reduction in the proof of Theorem 117.</figcaption></figure>

We use $\mathcal{L}_{\ge 0}$ and $\mathcal{L}_k$ as two sets of locations disjoint from $\mathcal{L}$ defined by

$$ \mathcal{L}_{\ge 0}^{\text{def}} = \{ \ell'_{\ge 0} \in \mathcal{L} \times \{1, \dots, k\} \mid \exists \ell \in \mathcal{L} \cdot (\ell \xrightarrow{i \xrightarrow{\ge 0}} \ell') \in A \} $$

$$ \mathcal{L}_k^{\text{def}} = \{ \ell_i \mid 1 \le i \le k \} $$

and define the set of actions by (see Figure 11.8)

$$ \begin{align*} A' &\stackrel{\text{def}}{=} \{ \ell \xrightarrow{\vec{e}_i} \ell' \mid (\ell \xrightarrow{\vec{e}_i} \ell') \in A \} \cup \{ \ell \xrightarrow{\vec{0}} \ell'' \mid (\ell \xrightarrow{\vec{e}_i} \ell'') \in A \} \\ &\cup \{ \ell \xrightarrow{\vec{0}} \ell'_{\ge 0}, \ell'_{\ge 0} \xrightarrow{\vec{0}} \ell', \ell'_{\ge 0} \xrightarrow{\vec{0}} \ell_i \mid (\ell \xrightarrow{\vec{0}} \ell') \in A \} \\ &\cup \{ \ell_i \xrightarrow{\vec{e}_j} \ell_i, \ell_i \xrightarrow{\vec{0}} \ell_{halt} \mid 1 \le i, j \le k, j \ne i \}. \end{align*} $$

We use $\ell_0(\vec{0})$ as initial configuration and $\ell_{halt}(\vec{0})$ as target configuration for the constructed configuration reachability instance. Here is the crux of the argument why Eve has a winning strategy to reach $\ell_{halt}(\vec{0})$ from $\ell_0(\vec{0})$ if and only if the Minsky machine halts, i.e., if and only if the Minsky machine reaches $\ell_{halt}(\vec{0})$. Consider any configuration $\ell(\vec{v})$. If $(\ell \xrightarrow{\vec{e}_i} \ell') \in A$, Eve has no choice but to apply $\ell \xrightarrow{\vec{e}_i} \ell'$ and go to the
configuration $\ell'(\vec{v} + \vec{e}_i)$ also reached in one step in $\mathcal{M}$. If $\{\ell \stackrel{i \xrightarrow{\sim}}{\to} \ell', \ell \stackrel{-\vec{e}_i}{\to} \ell''\} \in A$ and $\vec{v}(i) = 0$, due to the natural semantics, Eve cannot use the action $\ell \stackrel{-\vec{e}_i}{\to} \ell''$, thus she must use $\ell \stackrel{0}{\to} \ell'_{i \stackrel{\sim}{\to}}$. Then, either Adam plays $\ell'_{i \stackrel{\sim}{\to}} \stackrel{0}{\to} \ell'$ and Eve regains the control in $\ell'(\vec{v})$, which was also the configuration reached in one step in $\mathcal{M}$, or Adam plays $\ell'_{i \stackrel{\sim}{\to}} \stackrel{0}{\to} \ell_i$ and Eve regains the control in $\ell_i(\vec{v})$ with $\vec{v}(i) = 0$. Using the actions $\ell_{i \stackrel{\sim}{\to}} \stackrel{-\vec{e}_j}{\to} \ell_i$ for $j \neq i$, Eve can then reach $\ell_i(\vec{0})$ and move to $\ell_{halt}(\vec{0})$. Finally, if $\{\ell \stackrel{i \stackrel{\sim}{\to}}{\to} \ell', \ell \stackrel{-\vec{e}_i}{\to} \ell''\} \in A$ and $\vec{v}(i) > 0$, Eve can choose: if she uses $\ell \stackrel{-\vec{e}_i}{\to} \ell''$, she ends in the configuration $\ell''(\vec{v} - \vec{e}_i)$ also reached in one step in $\mathcal{M}$. In fact, she should not use $\ell \stackrel{0}{\to} \ell'_{i \stackrel{\sim}{\to}}$, because Adam would then have the opportunity to apply $\ell'_{i \stackrel{\sim}{\to}} \stackrel{0}{\to} \ell_i$, and in $\ell_i(\vec{v})$ with $\vec{v}(i) > 0$, there is no way to reach a configuration with an empty $i$th component, let alone to reach $\ell_{halt}(\vec{0})$. Thus, if $\mathcal{M}$ halts, then Eve has a winning strategy that mimics the unique play of $\mathcal{M}$, and conversely, if Eve wins, then necessarily she had to follow the play of $\mathcal{M}$ and thus the machine halts.

Finally, regarding the existential initial credit variant, the arguments used in the proof of Theorem 112 apply similarly to show that it is also undecidable. $\square$

In dimension one, Theorem 116 applies, thus configuration reachability is decidable in EXPSPACE. This bound is actually tight.

**Theorem 118** (Asymmetric vector games are EXPSPACE-complete in dimension one). *Configuration reachability asymmetric vector games, both with given and with existential initial credit, are EXPSPACE-complete in dimension one.*

*Proof.* Let us first consider the existential initial credit variant. We proceed as in Theorems 113 and 114 and reduce from the acceptance problem for a deterministic Turing machine working in exponential space $m = 2^{p(n)}$. The reduction is mostly the same as in Theorem 113, with a few changes. Consider the integer $m-n$ from that reduction. While this is an exponential value, it can be written as $m-n = \sum_{0 \le e \le p(n)} 2^e \cdot b_e$ for a polynomial number of bits $b_0, \dots, b_{p(n)}$. For all $0 \le d \le p(n)$, we define $m_d \stackrel{\text{def}}{=} \sum_{0 \le e \le d} 2^e \cdot b_e$; thus $m-n+1 = m_{p(n)}+1$.

We define now the sets of locations

$$ \mathcal{L}_{\text{Eve}} \stackrel{\text{def}}{=} \{ \ell_0, \odot \} \cup \{ \ell_{\gamma} | \gamma \in \Gamma' \} \cup \{ \ell_{\gamma}^k | 1 \le k \le 3 \} \cup \{ \ell_{=j} | 0 < j \le n \} \\ \cup \{ \ell_{1 \le ? \le m_d+1} | 0 \le d \le p(n) \} \cup \{ \ell_{1 \le ? \le 2^d} | 1 \le d \le p(n) \}, \\ \mathcal{L}_{\text{Adam}} \stackrel{\text{def}}{=} \{ \ell_{(\gamma_1, \gamma_2, \gamma_3)} | \gamma_1, \gamma_2, \gamma_3 \in \Gamma' \}. $$

The intention behind the locations $\ell_{=j} \in \mathcal{L}_{\text{Eve}}$ is that Eve can reach $\odot(0)$ from a configuration $\ell_{=j}(c)$ if and only if $c = j$; we define accordingly $A$ with the action $\ell_{=j} \stackrel{-j}{\to} \odot$. Similarly, Eve should be able to reach $\odot(0)$ from $\ell_{1 \le ? \le m_d+1}(c)$ for $0 \le d \le p(n)$ if and only if $1 \le c \le m_d+1$, which is implemented by the following actions: if $b_{d+1} = 1$, then

$$ \ell_{1 \le ? \le m_{d+1}+1} \stackrel{0}{\to} \ell_{1 \le ? \le 2^{d+1}}, \qquad \ell_{1 \le ? \le m_{d+1}+1} \stackrel{-2^{d+1}}{\longrightarrow} \ell_{1 \le ? \le m_{d+1}}, $$

and if $b_{d+1} = 0$,

$$ \ell_{1 \le ? \le m_{d+1}+1} \stackrel{0}{\to} \ell_{1 \le ? \le m_{d+1}}, $$