We simulate the choices of above in a turn-based game $\G' = \zug{V', E', T'}$. We define $V' = V \times \set{1,2, 3, 4}$, where $V'_1 = V \times \set{1,3}$ and $V'_2 = V \times \set{2,4}$. Suppose that the token is placed on $\zug{v, 1}$. This is associated with a configuration $\zug{v, P}$ in $\G$, where controls $v$, i.e., for $j$ such that $v \in V_j$, we have $j \in P$. The neighbors of $\zug{v, 1}$ is a set of intermediate vertices $\set{\zug{u, 4}: u \in N(v)}$, which represent the possible ways in which the token can move from $v$. chooses between (1) grabbing control of $u$, simulated by an edge to $\zug{u,2}$, and (2) allowing to move in $u$, simulated by an edge to $\zug{u, 1}$. Dually, the neighbors of $\zug{v, 2}$ are  $\set{\zug{u, 3}: u \in N(v)}$, and the other edges are similar. Finally, we define $T' = T \times \set{1,2}$. Note that the size of $\G'$ is clearly polynomial in the size of $\G$.

Let $c = \zug{v_0, P}$. We define $v'_0 = \zug{v_0, 1}$ if controls $v$ in the initial configuration $c$, and otherwise $v'_0 = \zug{v_0, 2}$. In App. <ref>, we prove that wins $\G$ from $c$ iff he wins $\G'$ from $v_0$. Since solving $\G'$ can be done in PTIME (Thm. <ref>), we have the following.

In this section, we show that MVPP always grabbing or giving games are in PTIME. We find it intriguing that a seemingly small change in the mechanism – allowing a choice between grabbing and giving instead of only grabbing – reduces the complexity to $\PTIME$ from $\EXP$-complete.
We make the following simple observation.

In an always grabbing or giving game, every time makes a move from a vertex $v$ to a vertex $u$, can decide which player controls $u$.

If does not control $p_{u}$ that owns $u$ and he wants to control $u$, he can grab $p_{u}$ from .
If he does not want to control $u$ and if he has $p_{u}$, he can give it to .

Consider an always-grabbing-or-giving game $\G = \zug{V, E, T}$ and an initial configuration $c$. We construct a turn-based game $\G'$ and an initial vertex $v_0$ so that wins in $\G$ from $c$ iff he wins in $\G'$ from $v_0$. Let $\G'=\zug{V', E', T'}$, where $V' = \{\zug{v,i}, \zug{\widehat{v},i} \:|\: v \in V, i \in \{1,2\}\}$ with $V_1'=\{\zug{v,1}, \zug{\widehat{v},1} \:|\: v \in V\}$ and $V_2'=\{\zug{v,2}, \zug{\widehat{v},2} \:|\: v \in V\}$, $T' = T \times \{1,2\}$, and $E' = \{(\zug{v,i}, \zug{\widehat{u},3-i}), (\zug{\widehat{u},3-i}, \zug{u,i}), (\zug{\widehat{u},3-i}, \zug{u,3-i}) \:|\: (v,u) \in E, i \in \{1,2\}\}$.
We call each vertex $\zug{v,i}$ a main vertex and each $\zug{\widehat{v},i}$ an intermediate vertex.
Suppose that moves the token from $v$ to $u$ in $\G$.
If decides to control $u$, then in $\G'$, the token moves from the main vertex $\zug{v,i}$ to the main vertex $\zug{u, 3-i}$, else from $\zug{v,i}$ to the main vertex $\zug{u, i}$, and in each case, through the intermediate vertex $(\widehat{u}, 3-i)$ that models the decision of on the control of $u$. The target vertices $T'$ are main vertices.

We can prove the following lemma.

Suppose wins from configuration $\zug{v,P}$ in $\G$. If he controls $v$, he wins from $\zug{v,1}$ in $\G'$, and if controls $v$, wins from $\zug{v,2}$ in $\G'$. Dually, suppose that wins from $\zug{v, P}$ in $\G$. If she controls $v$, then she wins from $\zug{v, 2}$ in $\G'$, and if controls $v$, wins from $\zug{v, 1}$ in $\G'$.

Suppose has a winning strategy in the game $\G$ from configuration $\zug{v,P}$.
We show that has a winning strategy in the game $\G'$ from vertex $\zug{v,i}$.
The other direction of the lemma follows from determinacy of two-player reachability games.
We prove the above for .
The proof for is analogous.

Let $W_j$ be the set of configurations in $\G$ such that has a strategy to reach $T$ in at most $j$ rounds.
Let $A_j$ be the set of vertices in $\G'$ such that has a strategy to reach $T'$ in at most $j$ rounds. We prove the following claim.

If $\zug{v,P} \in W_j$, with () controlling $v$ then $\zug{v, 1}$ ($\zug{v, 2}$) belongs to $A_{2j}$.

We prove this by induction on $j$. For the base case with $j=0$. this clearly holds.
Suppose the claim holds for $j=h$, and we now show that the claim holds for $j=h+1$.

Consider a configuration $\zug{v,P} \in W_{h+1}$.
We first look at the case when controls $v$.
We show that $\zug{v, 1} \in A_{2(h+1)}$.
Note that, by definition of $\G$ and $\G'$, both $\zug{v,P}$ and $\zug{v,1}$ are controlled by in $\G$ and $\G'$ respectively.

Since $\zug{v,P} \in W_{h+1}$ and controls vertex $v$, there is a strategy of that takes the token starting from $v$ with pawns $P$ to a target vertex in $T$ in at most $h+1$ steps.
Let under this strategy, moves the token from $v$ to $u$.

Note that $\zug{u, P'}\in W_h$ for all configurations $\zug{u, P'}$ that can reach after grabbing from or giving a pawn after moves the token from $v$ to $u$.
Let $P_u$ be the pawn owning vertex $u$.
Now from Observation <ref>, we know that once moves the token from vertex $v$

to a vertex $u$, then can reach a configuration $\zug{u, P'}$ with $p_u \in P'$ as well $\zug{u, P''}$ with $p_u \notin P''$.
Thus there exist configurations $\zug{u,P'},\zug{u,P''}$ in $W_h$ such that $p_u\in P'$ and $p_u\notin P''$.
Now suppose the token is at vertex $\zug{v,1}$ in $\G'$.
Since $u$ is a neighbour of $v$, by the definition of $\G'$, we have that vertex $\zug{\widehat{u},2}$ is a neighbour of $\zug{u,1}$ in $\G'$.
We show that $\zug{\widehat{u},2}\in A_{2h+1}$.
Recall that vertex $\zug{\widehat{u},2}$ is controlled by and the only neighbours of this vertex are $\zug{u,1}$ and $\zug{u,2}$.
Now if we show that both $\zug{u,1}$ and $\zug{u,2}$ are in $A_{2h}$, then we are done.

Since we know that there exists $\zug{u,P'}$ in $W_h$ such that $p_u\in P'$, by the induction hypothesis, we have that $\zug{u,1}\in A_{2h}$, and similarly since there exists $\zug{u,P''}$ in $W_h$ such that $p_u\notin P''$, we have that $\zug{u,2}\in A_{2h}$.

The case for which does not control $v$ can also be proved similarly.

We show that wins in $\G$ from $\zug{v,P}$ when () controls $v$ implies that wins from $\zug{v,i}$ ($\zug{v,3-i}$) in $\G'$.
By taking contrapositive, we have that loses from $\zug{v,i}$ ($\zug{v,3-i}$) in $\G'$ implies that loses in $\G$ from $\zug{v,P}$ when () controls $v$.
By determinacy, we have that wins from $\zug{v,i}$ ($\zug{v,3-i}$) in $\G'$ implies that wins in $\G$ from $\zug{v,P}$ when () controls $v$.

Hence showed.

Since the size of $\G'$ is polynomial in the size of $\G$, Thm. <ref> implies the following.

MVPP always-grab-or-give PAWN-GAMES is in PTIME.

§ K-GRABBING PAWN GAMES

In this section, we consider pawn games under $k$-grabbing in increasing level of generality of the mechanisms. We start with positive news.

In a k-Grab game with initial vertex $v_i$ if can reach vertex $v\neq v_i$ in $t<k$ grabs then he can reach and control vertex $v_i$ in at most $t+1$ Grabs.

Suppose that has a strategy to reach $v$ in t grabs. Let under this strategy he reaches $v$ from its incoming neighbour $u$. Now either grabs a pawn in the round along the edge $(u,v)$ or he does not grab.
If he does not grab a pawn then that means he reaches $u$ in $t$ grabs and now if he does not control pawn owning vertex $v$ then he can grab it and reach $v$ in t+1 grabs.
Now if grabs a pawn in the round along the edge $(u,v)$ then observe that he could have anyway reached $v$ without grabbing this pawn or by grabbing any other pawn, i.e. he could have reached vertex $v$ by grabbing the pawn owning the vertex $v$. Hence showed.

OVPP $k$-grabbing PAWN-GAMES is in $\PTIME$.

Let $k \in \Nat$, an OVPP $k$-grabbing game $\G = \zug{V, E, T}$, and an initial configuration $c = \zug{v_0, P_0}$, where we refer to $P_0$ as a set of vertices rather than pawns. Our algorithm solves a harder problem. It computes a minimum-grabbing function $\eta: V \rightarrow \Nat$ that labels each vertex $u \in V$ with the necessary and sufficient number grabs needed from $u$ to win. Formally, $\eta(u)$ is such that wins an $\eta(u)$-grabbing game played on $\G$ from configuration $\zug{u, P_0}$ but loses an $\big(\eta(u) - 1\big)$-grabbing game from configuration $\zug{u, P_0}$. The algorithm is depicted in Alg. <ref>. It calls the $\Call{Solve-Turn-Based-Game}$, which returns the set of vertices that are winning for in a turn-based reachability game, e.g., using attractor-based computation as in Thm. <ref>.

[1]
$\ell = 0$
$\exists u \in V$ that is not labeled by $\eta$
$W^1_\ell = \Call{Solve-Turn-Based-Game}{V_1= P_0, V_2 = V \setminus P_0, E, T}$
Define $\eta(u) = \ell$, for all $u \in W^1_\ell$ that is not yet labeled.
$B_\ell = \set{u \in V \setminus W^1_\ell: N(u) \cap W^1_\ell \neq \emptyset}$
$T = B^\ell$ and $\ell = \ell+1$.

Given an OVPP pawn game $\G = \zug{V, E, T}$ and a set of pawns $P_0 \subseteq V$ that controls, the algorithm returns a minimum-grabbing function $\eta: V \rightarrow \Nat$.

For the base case, consider the turn-based game $\G_0 = \zug{V, E, T}$ with $V_1 = P_0$. Let $W^1_0 \subseteq V$ denote 's winning region in $\G_0$. Clearly, for every $u \in W^1_0$, we have $\eta(v_0) =0$, and for every $u \notin W^1_0$, we have $\eta(v_0) \geq 1$. For the inductive step, suppose that for $\ell \geq 0$, the set $W^1_\ell = \set{u \in V: \eta(u) \leq \ell}$ has been found. That is, for every $u \notin W^1_\ell$, has a strategy that wins the $\ell$-grabbing pawn game $\G$ from configuration $\zug{u, P_0}$. We show how to find $W^1_{\ell+1}$ in linear time. Let the border of $W^1_\ell$, denoted $B_\ell$, be the set of vertices from which $W^1_\ell$ can be reached in one step, thus $B_\ell = \set{v \in V:v\notin W^1_\ell : N(v) \cap W^1_\ell \neq \emptyset}$.
Note that the vertices in $B_\ell$ are all controlled by since otherwise, such vertices will be in the set $W^1_\ell$.

Now we show that a vertex $u \notin W^1_\ell$ has $\eta(u) = \ell+1$ iff can force the game from configuration $\zug{u, P_0}$ to a vertex in $B_\ell$ in one or more rounds without making any grab.

wins from such a vertex $u$ by forcing the game into $B_\ell$, grabbing the pawn in $B_\ell$, and proceeding to $W_\ell$, where by the induction hypothesis, he wins with the remaining grabs.
Computing $W^1_{\ell+1}$ roughly entails a solution to a turn-based game with target set $B_\ell \cup W^1_\ell$.

Intuitively, we show that a vertex $u \notin W^1_\ell$ has $\eta(u) = \ell+1$ iff can force the game from configuration $\zug{u, P_0}$ to a vertex in $B_\ell$ without making any grabs and in a non-trivial manner. We compute $W^1_{\ell+1}$ as follows. Consider the turn-based game $\G_\ell = \zug{V, E, B_\ell \cup W^1_\ell}$ with $V_1 = P_0$. We say that wins non-trivially from $u \in V$ if he has a strategy $f$ that guarantees the following against any strategy: the resulting play is of the form $u=v_0, v_1, v_2,\ldots, v_m$ with $v_m \in (B_\ell \cup W^1_\ell)$ and it is non-trivial, meaning that $m \geq 1$. Note the difference from standard turn-based games: a target vertex $u \in B_\ell \cup W^1_\ell$ might be losing for when considering winning non trivially, e.g., when $u$ has an outgoing edge to a sink, no non-trivial play that starts in $u$ ends in a target vertex.

Let $U^1_\ell$ denote the set of vertices from which wins in $\G_\ell$ non-trivially. We describe an algorithm for finding $U^1_\ell$.
We construct a game $\G'_\ell$ in which we make a copy $u'$ of each vertex $u \in B_\ell$, and set the neighbors of $u'$ to be $\{v\in N(u): v\notin W^1_\ell \}$. Intuitively, if wins from $u'$ in $\G'_\ell$, he can win in $\G_\ell$ from $u$ in a non-trivial manner: since $u'$ is not winning in $\G'_\ell$, must make at least one step before entering $B_\ell$.
Let $U'$ be the winning set for in $\G'_\ell$.
It is not hard to see that $U^1_\ell = \set{u \notin B_\ell: u \in U'} \cup \set{u \in B_\ell: u' \in U'}$.

Let $u \in U^1_\ell$. We claim that if $u\notin W_{\ell}^1$ then $\eta(u) = \ell+1$. First, since $u\notin W_{\ell}^1$, by the induction hypothesis, $\eta(u) \geq \ell+1$. Next, we show that $\eta(u) = \ell+1$ by showing that wins the $(\ell+1)$-grabbing pawn game $\G$ from configuration $\zug{u, P_0}$. initially plays according to a strategy that forces the game to $B_\ell$ non-trivially without grabbing.
Suppose that is playing according to some strategy and the game visits $u'$ before visiting $u'' \in B_\ell$. Then, grabs $u''$, proceeds to $W^1_\ell$, and uses his winning $\ell$-grabbing strategy from there.

Let $u \notin U^1_\ell \cup W^1_\ell$. We claim that $\eta(u) > \ell+1$. Note that in order to reach $W^1_\ell$ and in particular reach $T$, the game must first visit $B_\ell$. Suppose that is following a winning strategy in $\G_\ell$.  Thus, in order to reach $B_\ell$, must grab $u' \notin B_\ell \cup W^1_\ell$. Suppose that the game reaches a configuration $\zug{u'', P_0 \cup \set{u'}}$, where $u'' \in B_\ell$. By the above, $\eta(u'') \geq \ell+1$. That is, any strategy that wins from $u''$ must make at least $\ell+1$ grabs. Hence, in order to win from $u$, makes at least $\ell+2$ grabs.

Let $n = |V|$. Note that $W^1_n = V$. Computing $W^1_{\ell+1}$ from $W^1_\ell$ requires a call to an algorithm that solves a reachability game, which can be done in linear time. Hence, the total running time of the algorithm is polynomial in the size of $\G$.

@xc/pgf/inner xsep
@x by 2@xc
@xb/pgf/minimum width

@y by
@yc/pgf/inner ysep
@y by 2@yc
@yb/pgf/minimum height

@x by.5
@xa/pgf/outer xsep
@x by#1@xa
@y by-.5
@y by.5
@ya/pgf/outer ysep
@y by#1@ya

in east,west in north,mid,base,south

in east,west,north,mid,base,south,center,text

[node distance=8mm,initial text = ,main/.style = draw,circle, text=black, inner sep=1pt,main1/.style = draw,circle, blue, left color=blue!20, text=black, inner sep=1pt,main2/.style = draw,circle, red, left color=red!20, text=black, inner sep=1pt,main3/.style = draw,circle, green, left color=green!20, text=black, inner sep=1pt,gain1/.style = draw,square, blue, left color=blue!20, text=black, inner sep=1pt,gain2/.style = draw,square, red, left color=red!20, text=black, inner sep=1pt,gain3/.style = draw,square, green, left color=green!20, text=black, inner sep=1pt]
[main,initial] (1) 1;
[gain1] (2) [above right of=1] $S_1^1$;
[gain2] (3) [below right of=1] $S_2^1$;
[main] (4) [below right of=2] 2;
[gain3] (5) [below right of=4] $S_3^2$;
[gain2] (6) [above right of=4] $S_2^2$;
[main] (7) [above right of=5] $3$;
[gain3] (8) [right of=7] $S_3^3$;
[main,accepting] (9) [right of=8] $t$;
[main] (10) [right of=6] $s$;
[main] (11) [right of=5] $s$;
[->] (1) – (2);
[->] (1) – (3);
[->] (2) – (4);
[->] (3) – (4);
[->] (4) – (5);
[->] (4) – (6);
[->] (6) – (7);
[->] (5) – (7);
[->] (7) – (8);
[->] (2) to [out=90,in=90,looseness=0.5] (10);
[->] (6) – (10);
[->] (3) to [out=270,in=270,looseness=0.5] (11);
[->] (5) – (11);
[->] (8) – (10);
[->] (8) – (9);

Consider the input to SET-COVER $U = [3]$ and $\S = \set{\set{1}, \set{1,2}, \set{2,3}}$.
The figure depicts the output on this input of the reduction in

Thm. <ref>

The following theorem considers a constrained variant of $k$-grabbing: grabs, and she is only allowed to grab after moves. Interestingly, this is the only mechanism for which we obtain hardness results above PTIME for OVPP games.

OVPP constrained $k$-grabbing PAWN-GAMES is coNP-hard.

Recall that the input to SET-COVER is a universe $U = [n]$, a collection of sets $\S = \set{S_1,\ldots,S_m}$, where $S_i \subseteq U$, for each $1 \leq i \leq m$, and a number $k \in \N$. The goal is to decide whether there is a set cover of size $k$, namely a collection $\S' \subseteq \S$ and $\bigcup_{S \in \S'} S = U$ with $|\S'| = k$.
In Appendix <ref>, we show a reduction from the complement of SET-COVER, which is illustrated on the left side of Fig. <ref>. Intuitively, the game proceeds in rounds. At $v_0$, challenges by choosing $i \in U$. This allows to grab a vertex. She grabs a set $S_j$ that covers $i$, moves the token to $S_j$, and from there back to $v_0$. Note that moving to $S_j$ without grabbing it allows to win by proceeding to his target $t$.

Constrained $k$-grabbing pawn games with Büchi games objectives are NP-hard.

[node distance=8mm,initial text = ,main/.style = draw,circle, text=black, inner sep=1pt,main1/.style = draw,circle, blue, left color=blue!20, text=black, inner sep=1pt,main2/.style = draw,circle, red, left color=red!20, text=black, inner sep=1pt,main3/.style = draw,circle, green, left color=green!20, text=black, inner sep=1pt,gain1/.style = draw,square, blue, left color=blue!20, text=black, inner sep=1pt,gain2/.style = draw,square, red, left color=red!20, text=black, inner sep=1pt,gain3/.style = draw,square, green, left color=green!20, text=black, inner sep=1pt]
[main,initial] (1) 1;
[gain1] (2) [above right of=1] $S_1^1$;
[gain2] (3) [below right of=1] $S_2^1$;
[main] (4) [below right of=2] 2;
[gain3] (5) [below right of=4] $S_3^2$;
[gain2] (6) [above right of=4] $S_2^2$;
[main] (7) [above right of=5] $3$;
[gain3] (8) [right of=7] $S_3^3$;
[main,accepting] (9) [right of=8] $t$;
[main] (10) [right of=6] $s$;
[main] (11) [right of=5] $s$;
[->] (1) – (2);
[->] (1) – (3);
[->] (2) – (4);
[->] (3) – (4);
[->] (4) – (5);
[->] (4) – (6);
[->] (6) – (7);
[->] (5) – (7);
[->] (7) – (8);
[->] (2) to [out=90,in=90,looseness=0.5] (10);
[->] (6) – (10);
[->] (3) to [out=270,in=270,looseness=0.5] (11);
[->] (5) – (11);
[->] (8) – (10);
[->] (8) – (9);

Consider the input to SET-COVER $U = [3]$ and $\S = \set{\set{1}, \set{1,2}, \set{2,3}}$.
The figure depicts the output on this input of the reduction in

Thm. <ref>

The proof of the following theorem, which

is obtained by a reduction from SET-COVER.

MVPP $k$-grabbing game PAWN-GAMES is NP-hard.

Given an input $\zug{U, \S, k}$ to SET-COVER, we construct an MVPP $k$-grabbing pawn game $\G = \zug{V, E, T}$ in which grabs (see Fig. <ref>). Intuitively, $\G$  has a “chain-like” structure, and in order to win, must cross the chain. Certain positions in $\G$ corresponds to $i \in U$. Each neighbor of $i$ correspond to a set $S \in \S$ with $i \in S$. Thus, a choice of at $i$ can be thought of as assigning a set in $\S$ that covers $i$. We construct $\G$ so that before moving to a neighbor $S$ of $i$, must grab the pawn that owns $S$.
All vertices that correspond to $S$ are controlled by the same pawn, thus if moves from $i' > i$ to a neighbor that corresponds to $S$, there is no need to grab again. Since is allowed only $k$ grabs, there is a one-to-one correspondence between winning strategies and set covers of size $k$.

We describe the construction of $\G$ formally. Let $V = U \cup (\S \times U) \cup \set{s, t}$. 's target is $t$ and $s$ is a vertex with no path to $t$, thus it can be thought of as a target for . There are $m+1$ pawns. For $j \in [m]$, Pawn $j$ owns all vertices in $\set{\zug{S_j, i}: i \in U}$. Pawn $0$ owns the vertices in $U$. We describe the edges. For $i \in U$, we define $N(i) = \set{\zug{S_j, i}: i \in S_j}$. For $1 \leq i \leq n-1$ and $j \in [m]$, we define $N(\zug{S_j, i}) = \set{i+1, s}$ and $N(\zug{S_j, n}) = \set{t, s}$. That is, if moves from $i$ to its neighbor $S_j$ without controlling Pawn $j$, then will proceed to $s$ and win the game.

We claim that a set cover $\S'$ of size $k$ gives rise to a winning $k$-grabbing strategy. Indeed, by choosing, for each $i \in U$, to move to $S \in \S'$ and grabbing it if it has not been grabbed previously, guarantees that $t$ is reached using at most $k$ grabs. On the other hand, observe a play of a winning $k$-grabbing strategy against a reasonable strategy; namely, a strategy that always moves to $s$ from a neighboring vertex $u$ when controls $u$. Suppose that the set of pawns $\S'$ is grabbed. It is not hard to see that $\S'$ is a set cover of size at most $k$, and we are done.

We conclude this section by studying OMVPP games.

OMVPP $k$-grabbing PAWN-GAMES is PSPACE-hard.

Consider an input $\phi = Q_1 x_1 \ldots Q_n x_n C_1 \wedge \ldots \wedge C_m$ to TQBF, where $Q_i \in \set{\exists, \forall}$, for $1 \leq i \leq n$, each $C_j$, for $1 \leq j \leq m$, is a clause over the variables $x_1, \ldots, x_n$. We construct an OMVPP $n$-grabbing pawn game $\G = \zug{V, E, T}$ such that wins iff $\phi$ is true.

We describe the intuition and the details can be found in App. <ref>. The structure of
$\G$ is chain-like. needs to cross the chain in order to win. The first part of the chain requires to grab, for each variable $x_i$, either a pawn $p_i$ or a pawn $\neg p_i$. For existentially-quantified variables, decides which of the two is grabbed, and for universally-quantified variables, decides. In the second part of $\G$, we verify that the corresponding assignment is valid. Certain positions of $\G$ correspond to a clause $C_j$, for $j \in [m]$, which must take control over during the first part of $\G$. The key is to use OMVPP: We define that if $x_i$ appears in $C_j$, then $p_i$ is an owner of $C_j$, and if $\neg x_i$ appears in $C_j$, then $\neg p_i$ is an owner of $C_j$.
Thus, controls $C_j$ iff he grabbed a pawn that owns $C_j$ which is iff the assignment satisfies $C_j$.

The intuition is similar to Thm. <ref>. We construct $\G$ to have a chain-like structure that must cross in order to win. The chain consists of two parts. In the first part, each position corresponds to a variable $x_i$, for $i \in [n]$. We construct $\G$ so that if $x_i$ is existentially quantified, then controls $x_i$, and if $x_i$ is universally quantified, then controls $x_i$ and cannot win by grabbing it. We associate a move in $x_i$ with an assignment to $x_i$. Technically, $x_i$ has two neighbors $v_i$ and $\neg v_i$, initially at the control of . If the token reaches a neighbor of $x_i$ without grabbing it, then loses the game. is allowed $n$ grabs, thus in order to win, it is necessary for him to grab, for each $i$, one of the neighbors of $x_i$. It follows that a play that crosses the first part of the chain gives rise to an assignment $f$ to $x_1,\ldots, x_n$.

In the second part of $\G$, we verify that $f$ is valid. Each position of $\G$ corresponds to a clause $C_j$, for $j \in [m]$, all of which are at the control of in the initial configuration of $\G$. Note that once the first part of $\G$ is crossed,  is not allowed any more grabs. The idea is that when arriving at $C_j$, for $j \in [m]$, must control $C_j$, otherwise he loses. Recall that in OMVPP, it suffices to control one of the pawns that owns $C_j$ in order to control it. We define the pawns that own $C_j$ as follows. For $i \in [n]$, call $p_i$ the pawn that owns $v_i$ and $\neg p_i$ the pawn that owns $\neg v_i$. Thus, grabbing $p_i$ and $\neg p_i$ respectively corresponds to an assignment that sets $x_i$ to true and false. If $x_i$ appears in $C_j$, then $p_i$ is an owner of $C_j$, and if $\neg x_i$ appears in $C_j$, then $\neg p_i$ is an owner of $C_j$. Thus, controls $C_j$ iff $f(C_j) = \text{true}$. It follows that wins iff $f$ is valid.

Formally, the vertices of $\G$ are $V = \set{s, t} \cup \set{x_i, v_i, \neg v_i: 1 \leq i \leq n} \cup \set{C_j: 1 \leq j \leq m}$.
The target vertex is $t$. The vertex $s$ is a sink vertex that is winning for , i.e., there is no path from $s$ to $t$. The game consists of $2n+2$ pawns. For each $1 \leq i \leq n$, we associate with variable $x_i$ two pawns, which we denote by $p_i$ and $\neg p_i$. Intuitively, we will construct the game such that in order to win, must grab either $p_i$ or $\neg p_i$, and we associate grabbing $p_i$ and $\neg p_i$ with an assignment that sets $x_i$ to true and false, respectively. Formally, if $x_i$ appears in $C_j$, then $p_i$ is an owner of $C_j$, and if $\neg x_i$ appears in $C_j$, then $\neg p_i$ is an owner of $C_j$.
We use $1$ and $2$ to refer to the final two pawns.
Pawn $1$ owns every vertex $x_i$ such that variable $x_i$ is existentially quantified in $\phi$ and Pawn $2$ owns every vertex $x_i$ such that $x_i$ is universally quantified in $\phi$. In the initial configuration, controls only Pawn $1$.

We describe the edges in the game, which has a chain-like structure. The last vertex on the chain is the target $t$, thus must cross the chain in order to win.
We assume that follows a reasonable strategy; namely, a strategy that proceeds to win at $s$ given the option, i.e., when the game reaches a vertex $u$ at her control and that neighbors $s$.
The token is initially placed on $x_0$. For $1 \leq i \leq n$, the neighbors of $x_i$ are $v_i$ and $\neg v_i$. We associate with the choice at $x_i$, an assignment to $x_i$ in the expected manner.
Suppose that the token is placed on $u \in \set{v_i,\neg v_i}$. We require to grab the pawn that owns $u$ by adding an edge from $u$ to $s$. That is, since initially controls the pawn that owns $u$, if does not grab it, will win from  $u$. For $1 \leq i < n$, the neighbor of $v_i$ and $\neg v_i$ is $v_{i+1}$. The neighbor of $v_n$ and $\neg v_n$ is $C_1$.

Suppose that follows a strategy that leads the token to $C_1$. We observe that since Pawn $1$ is controlled by , chooses the assignment of the existentially-quantified variables.
We claim that 's strategy does not grab Pawn $2$, thus chooses the assignment of the universally-quantified variables.
Indeed, since is restricted to grab at most $n$ pawns and must grab either $p_i$ or $\neg p_i$, for each $1 \leq i \leq n$. If he grabs Pawn $2$, then there exists $1 \leq i \leq n$ such that he cannot grab any of $p_i$ or $\neg p_i$, and the game will necessarily reach either $v_i$ or $\neg v_i$ at the control of , from which she wins.

We describe the outgoing edges from clause vertices.
For $1 \leq j <m$, the vertex $C_j$ has two neighbors, $s$ and $C_{j+1}$, and the neighbors of $C_m$ are $s$ and $t$. That is, in order to draw the game to $t$, must cross all clause vertices. Recall that the definition of OMVPP dictates that chooses how to move the token at a vertex $u$ if he controls at least one of the pawns that owns $u$. Thus, a winning strategy must grab, for each $1 \leq j \leq m$, at least one pawn that owns $C_j$. In turn, grabbing a pawn that owns $C_j$ means that the assignment to $x_1,\ldots,x_n$ that arises from the players' strategies satisfies $C_j$. It follows that wins the game iff $\phi$ is true.

We turn to study the upper bound. The following lemma bounds the provides a polynomial bound on the length of a winning play for . The core of the proof intuitively shows that we can restrict attention to strategies that grab at least once in a sequence of $|V|$ rounds. Otherwise, the game enters a cycle that is winning for .
We thus obtain a polynomial bound on the length of a winning play for .

Consider an OMVPP $k$-grabbing PAWN-GAME $\G = \zug{V, E, T}$, and an initial configuration $c$ that is winning for .
Then, has a strategy such that, for every strategy, a target in $T$ is reached within $|V| \cdot (k+1)$ rounds.

Consider the turn-based game $\G'$ that corresponds to $\G$. Recall that $c$ is a vertex in $\G'$. Fix a memoryless winning strategy in $\G'$, which exists since $\G'$ is a turn-based reachability game. Consider some strategy and let $\pi$ be the resulting play. We make three observations. (1) Each vertex in $\G'$ is visited at most once by $\pi$. Otherwise, $\pi$ enters a loop, which is losing for . (2) The configurations can be partially ordered: a configuration $(v, P)$ can only be visited before a configuration $(u, P')$, for $P \subseteq P'$. Indeed, the only manner in which control of pawns changes is by grabbing, which only adds pawns to the set that he already controls. (3) If the game starts from $(v, P)$, then it ends in a configuration $(u, P')$ with $|P'| \leq |P| + k$. Indeed, can only grab $k$ times. Combining (1)-(3) implies that $\pi$ visits $T$ within $|V| \cdot (k+1)$ rounds.

Suppose has a winning strategy, and since we consider a reachability objective, in the configuration graph he has one which is a memoryless strategy.
We call this strategy $\sigma_1$.
We fix a memoryless strategy of and consider the resulting play $\pi$.
Suppose for contradiction, we have that $\pi$ visits a target state in more than $n \cdot (k+1)$ steps.
Since grabs at most $k$ pawns, this implies that there exists a sequence of $n$ steps and a configuration $\zug{v,P}$ within the first $n \cdot (k+1)$ steps such that the configuration $\zug{v,P}$ is visited at least twice in this sequence of $n$ steps.
This implies that the the play $\pi$ contains an infix which forms a loop on the configuration graph, and does not grab a pawn in this loop.
Since both players have memoryless strategies, this implies that the play always takes this loop and never reaches a target state contradicting that $\sigma_1$ is winning for .
This implies that every $n$ steps, should grab at least one pawn and the play thus reaches a target state in $n \cdot (k+1)$ steps.

For the upper bound,

we describe an algorithm performing a depth-first traversal of the configuration graph of a game while storing, at a time, only a branch in $\PSPACE$.

OMVPP $k$-grabbing PAWN-GAMES is in $\PSPACE$.

We describe a $\PSPACE$ algorithm for OMVPP $k$-grabbing PAWN-GAMES as follows.

The algorithm explores an unwinding of the configuration graph of the $k$-grabbing pawn game in a depth-first manner.
We call this unwinding of the configuration graph a game tree.
Recall that after each move by a player in the game, chooses to grab a pawn and if is controlling the current vertex, that is, where the token lies, then chooses a successor, otherwise chooses a successor.
A vertex $v$ that is controlled by is an OR-vertex in the game tree in the sense that there should exist a successor of $v$ which accepts.
On the other hand, a vertex $v$ that is controlled by is an AND-vertex in the game tree in the sense that all the successors of $v$ should accept.

Since by Lemma <ref>, if has a winning strategy then he has one such that for all strategies of , he wins in $n \cdot (k+1)$ steps,

it is sufficient to unwind the configuration graph such that the length of a path in the game tree starting from the initial vertex does not exceed $n \cdot (k+1)$.
At any time during exploring the game tree in a depth-first manner, the algorithm stores the path that is being currently traversed from the initial vertex, and the length of the path is thus at most $n \cdot (k+1)$.
In a depth-first traversal, from each vertex, its successors are visited in a particular order.
At each level of the path that has been currently traversed, the algorithm also keeps count of how many successors of the vertex at that level have been visited, and also the depth of the level from the root of the tree.
The latter ensures that the algorithm does not unwind the configuration graph to an extent so that the length of a path in the game tree exceeds $n \cdot (k+1)$.
Since in the configuration graph, there are at most exponentially many vertices of the form $\zug{v, P}$ where $v$ is a vertex of the $k$-grabbing pawn game and $P$ is a set of pawns, at each level, the count of number of successors that have been visited so far can be stored in $\PSPACE$.
Since the number of levels of the current path is bounded by $n \cdot (k+1)$ which is polynomial and each level uses polynomial space, the algorithm is in $\PSPACE$.

By Lem. <ref>, each branch of such a traversal has polynomial length, leading to the PSPACE upper bound.
We thus have the following.

OMVPP $k$-grabbing PAWN-GAMES is PSPACE-complete.

We also note that in the case of $k$-grabbing mechanism, unlike optional-grabbing or always-grabbing mechanisms, it is always the case that for , at every vertex, controlling more pawns is at least as good as controlling fewer pawns.
This is because, if needs to control a particular vertex $v$ in any round of the game in order to win, he can grab the pawn controlling the vertex $v$ if the pawn does not belong to him regardless of which player moves the token provided he has not already grabbed $k$ pawns.

§ DISCUSSION

We introduce pawn games, a class of two-player turn-based games in which control of vertices  changes  dynamically throughout the game. Pawn games constitute a class of succinctly-represented turn-based games.
We identify natural classes that are in PTIME. Our EXPTIME-hardness results are based on games, which we hope will serve as a framework for proving lower bounds.

We mention directions for future research. First, we leave several open problems; e.g., for MVPP $k$-grabbing pawn games, we only show NP-hardness and membership in PSPACE. Second, we focused on reachability games. It is interesting to study pawn games with richer objectives such as parity or quantitative objectives.
Quantitative objectives are especially appealing since one can quantify the benefit of controlling a pawn.
Third, it is interesting to consider other pawn-transferring mechanisms and to identify properties of mechanisms that admit low-complexity results. Finally, grabbing pawns is a general concept and can be applied to more involved games like stochastic or concurrent games.

§ PROOFS FROM SECTION <REF>

§.§ Proof of Thm. <ref>

For the base case, we prove for both $i=0$ and $i=1$. Recall that the target set of $\G'$, which coincides with $W_0$, consists of configuration vertices whose $V$ component is in $T$. Thus, for the first part of the claim, since $c \in W_0$, then $v \in T$, and thus $\zug{v, P'} \in W_0$. Recall that an intermediate vertex is of the form $\zug{u, b}$, where $u$ denotes the “next” location of the token and $b$ denotes the “previous” configuration. In the case of $W_1$, since wins in one turn, each vertex in $W_1$ is of the form $\zug{u, b}$, where $u \in T$. Thus, for $\zug{u,c}\in W_1$, we clearly have $\zug{u,c'}\in W_1$.

For the induction hypothesis, assume that the claim holds for $i=n$, and we prove for $i=n+1$.
We start with configuration vertices.
Assume $c=\zug{v,P}\in W_{n+1}$.
We will show that $c'=\zug{v,P'}\in W_{n+1}$.
Recall that $N(c)$ consist of intermediate vertices of the form $\zug{u, c}$, where $u \in N(v)$, thus $\zug{u, c} \in N(c)$ iff $\zug{u, c'} \in N(c')$. Note that if $\zug{u, c} \in N(c)$ is winning for , i.e., $\zug{u, c} \in W_n$, then by the induction hypothesis, $\zug{u, c'} \in W_n$. We distinguish between two cases.
In the first case, controls $c$, i.e., $j\in P$ and $c$ is a vertex. In this case, our assumption is that $c'$ is also a vertex. Since $c \in W_{n+1}$, there must exist a neighbor $\zug{u, c}$ of $c$ having $\zug{u,c} \in W_n$. By the above, $\zug{u, c'} \in (N(c') \cap W_n)$, thus $c' \in W_{n+1}$. In the second case, controls $c$, thus $j\notin P$. Recall that $P' \subseteq P$, thus controls $c'$ as well. Note that $c \in W_{n+1}$ implies that wins from all of its neighbors. By the above, wins from all the neighbors of $c'$, thus $c' \in W_{n+1}$.

We turn to the second part of the claim that addresses intermediate vertices.
We again distinguish between two cases: $j \in P$ and $j \notin P$.
Consider an intermediate vertex $\zug{u, c} \in W_{n+1}$.
We will show that $\zug{u, c'} \in W_{n+1}$.
We denote by $\ell$, the pawn that owns $u$.

Recall that in optional grabbing, has the option of grabbing after moves, thus $\zug{u, c}$ is a vertex.
Since the claim requires that if $j \in P$, then $j \in P'$, we conclude that $\zug{u, c'}$ is also a vertex.
Consider a neighbor of $\zug{u, c'}$, a configuration vertex $\zug{u,Q'}$.
Note that either does not use the option to grab, then $Q'=P'$, or she grabs a pawn $r$ from , then $Q'=P' \setminus \set{r}$.
Note that in order to apply the induction hypothesis on $\zug{u, Q'}$, we need to find a neighbor $\zug{u, Q}$ of $\zug{u, c}$ such that if $\ell \notin Q'$, then $\ell \notin Q$.
Note that at $\zug{u, c}$, has the option of not grabbing as well as of grabbing $\ell$, thus both $\zug{u, P}$ and $\zug{u, P\setminus \set{\ell}}$ are neighbors of $\zug{u, c}$. Note that $P = P \setminus \set{\ell}$ when $\ell \notin P$. That is, cannot grab $\ell$ when she already owns it. Since $\zug{u, c} \in W_{n+1}$ and it is a vertex, both $\zug{u, P} \in W_n$ and $\zug{u, P\setminus \set{\ell}}
\in W_n$.
Finally, if $\ell \in Q'$, define $Q := P$, and if $\ell \notin Q'$, define $Q := P \setminus \set{\ell}$.
In both cases, since $Q' \subseteq P'$ and $P' \subseteq P$, we have $Q' \subseteq Q$ and meets the requirement in the claim on $\ell$.
Thus, since $\zug{u, Q} \in W_n$, by the induction hypothesis, $\zug{u, Q'} \in W_n$.
Since $\zug{u, Q'}$ is any arbitrary neighbour of the vertex $\zug{u,c'}$, we have that $\zug{u,c'} \in W_{n+1}$.

In the second case $j\notin P$. That is, makes the move in $\zug{v, P}$, and thus $\zug{u, c}$ is a vertex. Since $P' \subseteq P$, we have $j \notin P'$, thus $\zug{u, c'}$ is also a vertex. Since $\zug{u, c} \in W_{n+1}$, it has a neighbor $\zug{u, Q} \in W_n$.
Note that since either grabs or does not grab in $\zug{u, c}$, we have $P \subseteq Q$. We find a neighbor $\zug{u, Q'}$ of $\zug{u, c'}$ to apply the induction hypothesis on.
Note that has the option to grab at $\zug{u, c'}$, and, among his choices, he can choose not to grab or to grab $\ell$.
If $\ell \in Q$, then we choose $Q' := P' \cup \set{\ell}$, and if $\ell \notin Q$, we choose $Q' := P'$. In both cases, $Q' \subseteq Q$ and meets the requirement in the claim.
Thus, since $\zug{u,Q} \in W_n$, by the induction hypothesis, we have $\zug{u, Q'} \in W_n$, and hence $\zug{u,c'} \in W_{n+1}$.

§.§ Proof of Thm. <ref>

Consider an input OVPP optional-grabbing game $\G = \zug{V, E, T}$ and an initial configuration $\zug{v_0,P_0}$. Correctness of the algorithm follows from the two following claims. First, we show soundness; namely, whenever the algorithm returns that wins, he does indeed have a winning strategy from $\zug{v_0, P_0}$.

For $i \geq 0$, wins from every vertex $v \in W_i$ no matter who makes the last step into $v$.

The proof is by induction on $i$. The base case is trivial since $W_0 = T$. For the inductive step, suppose that the claim holds for $W_i$ and we show that it holds in all ways that it can be extended.

Case 1 – Line $4$: for a vertex $u$ having $N(u) \subseteq W_i$, wins no matter who controls $u$ since in the next turn, $W_i$ is necessarily reached.

Case 2 – Line $10$: We claim that wins from $u \in B'$ no matter who controls $u$. Indeed, if controls $u$, he wins by proceeding to $W_i$. If controls $u$ and avoids $W_i$, then the next vertex is necessarily in $B$. grabs and proceeds to $W_i$.

Case 3 – Line $12$: Let $v\in R\setminus P_0$.
can always ensure that controls $v$ by never grabbing $v$.
Also in OVPP optional-grabbing, does not need to grab $v$ in order to reach $v$.
Thus if has a strategy such that the token reaches $v$, then he can ensure that the token reaches $v$ and is controlled by .

Hence, once $v$ is reached, since it is controlled by , she is forced to move from $v$ to a vertex $v'$ in $B$.
then grabs $v'$ unless he already controls it and moves the token to $W_i$.

We turn to prove completeness.

Suppose that the algorithm terminates at iteration $i$ in Lines $7$ or $13$. Then, has a winning strategy from $\zug{v_0, P_0}$.

We first consider the case of terminating in Line $7$. Thus, every vertex not in $W_i$, including $v_0$, does not have a path to $W_i$. Clearly wins.

Second, suppose that the algorithm terminates in Line $13$. We describe a winning strategy from $\zug{v_0, P_0}$ that avoids $W_i$.
Whenever moves the token, she moves it to an arbitrary vertex not in $W_i \cup B$. When the token reaches $u \in B$, it is following a move, and grabs $u$, and moves to $W_i \cup B$.

We claim that wins when the game starts from $\zug{v_0, P_0}$. Assume towards contradiction that $W_i$ is reached. Since $v_0 \notin W_i$, a visit to $W_i$ must first visit a vertex $u \in B$. We claim that (i) $u$ is in the control of and that (ii) she can move away from $W_i$. Combining (i) and (ii) we reach a contradicting to the assumption that $W_i$ is reached. We conclude the proof by showing that (i) and (ii) hold.
For (ii), note that $u$ has a neighbor not in $W_i \cup B$ otherwise $u$ would have been added to $W_{i+1}$ in Line $4$ or Line $12$.
We turn to prove (i). Suppose first that $u=v_0$.
If controls $v_0$, then the algorithm terminates in Line $8$.
Since it does not terminate there, controls $u$.
Next we consider the case that $u \neq v_0$, thus $u$ has a predecessor $u'$ in the play.
We distinguish between two cases.
If $u' \in R$, then $u' \in P_0$ otherwise it would have been added to $W_{i+1}$ in Line $12$.
Thus, makes the move from $u'$ to $u$, and grabs $u$ following 's move (if she does not control it already).
The second case is when $u' \notin R$.
Recall that a vertex is in $R$ if all of its neighbors lead to $B$, thus $u' \notin R$ implies that it has at least one neighbor not in $B$.
Note that if $u'$ was in the control of , her strategy would have dictated to proceed to a vertex not in $B$.
Thus, if makes the move from $u'$ to $u$, and grabs $u$ following 's move.

§.§ Algorithm for OVPP Optional Grabbing Pawn Games

OVPP optional-grabbing game $\G = \zug{V, E, T}$ and an initial configuration $\zug{v_0,P_0}$.

$\zug{V, E, T},\zug{v_0,P_0}$

$v_0\in T$

$T' = T \cup \set{u: N(u) \subseteq T}$

$T'\neq T$
$\zug{V, E, T'},\zug{v_0,P_0}$

$B := \set{u: N(u) \cap T \neq \emptyset}$

$B' = \set{u \in B: N(u) \subseteq B \cup T}$

$B'\neq \emptyset$
$\zug{V, E, T\cup B'},\zug{v_0,P_0}$
$v_0\in B$ and $v_0\in P_0$

$R = \set{u: N(u) \subseteq B}$

$R \setminus P_0 \neq \emptyset$$\zug{V, E, T\cup R\setminus P_0},\zug{v_0,P_0}$

A plain algorithm

(1)  Note reaching $Q$ ensures reaching $T$ as if its who controls vertex in $Q$ he can move the token to $T$ and if its who controls the vertex in $Q$ then he can either move the token to T or to one of the vertex in W in which case can control the target vertex and move the token to T.

(2) Observe that for token to reach the target set it has to pass through $W$.
Also note that vertex in $W$ always has an edge that can take the token  away from $TUW$.
Thus for to win he should be controlling the vertex when the token reaches $W$.
This is only possible when the last move before reaching $W$ is played by , because if it is played by then can always grab the pawn controlling the target vertex.
Thus for moving the token to $W$ is a losing move, hence this move has to be forced.
Note $R$ is set of those vertices from where if controls the vertex, he is forced to move in $W$.

Note for to win he should ensure game reaches $R$ and it is who controls the vertex with the token. Now if $R\subseteq I_1$ then a simple strategy for that involves not grabbing of pawns controlling vertices in $R$, would ensure win for .

Using lemma 3 if you can reach $R'$ you can reach $R'$ and ensure controls the vertex with the token in $R'$

§.§ Proof of Thm. <ref>

$\G'$ in which every vertex is a configuration $\zug{v,A}$ of $G$.
A vertex $\zug{v,A}$ in $\G'$ belongs to iff vertex $v$ in $\G$ belongs to .

Note that the size of $\G'$ is exponential in the number of locks since $A \subseteq L$.
The set $T'$ target states in $\G'$ are defined as $T' = \set{(v, A) \:|\: v \in T}$.
It is easy to see that there exists a strategy of to reach $T'$ in $\G'$ there exists a strategy of to reach $T$ in $\G$.
The EXPTIME membership follows since reachability games can be solved in time polynomial in the size of the input arena.

An ATM is $\zug{Q, \Gamma, \delta, q_0, q_{acc}, q_{rej}}$, where $Q$ is a collection of states that is partitioned into $Q = Q_1 \cup Q_2$, $\Gamma$ is a tape alphabet, $\delta: Q \times \Gamma \rightarrow 2^{Q \times \Gamma \times \set{L, R}}$ is a transition function, $q_0, q_{acc}, q_{rej} \in Q$ are respectively an initial, accepting, and rejecting states.
Let $w\in\Sigma^*$ be an input word, and let $m\in\N$ be
a bound on the length of the tape used when running $w$ on the machine.
Since we consider a polynomial space machine, $m$ is polynomial in the length of $w$.
A configuration of an ATM is $\zug{q, \pos, \zug{\gamma_1,\ldots, \gamma_m}}$, where $q \in Q$ denotes the current control state of the machine, $i \in \set{1,\ldots, m}$ is the position of the head on the tape, and $\zug{\gamma_1,\ldots, \gamma_m} \in \Gamma^m$ denotes the tape contents. The player who controls $q$ chooses an outgoing transition $t \in \delta(q, \gamma_\pos)$. Let $t = \zug{q', \gamma', B}$.
Then, the next control state is $q'$, the tape head moves to $\pos+1$ if $B = R$ and to $\pos-1$ if $B=L$, and the $\pos$-th tape content changes from $\gamma_\pos$ to $\gamma'$.
W.l.o.g., we assume that for every input, the Turing machine we consider above halts, and the input is accepted if and only if it halts in $q_{acc}$.

We show that solving games is EXPTIME-complete.
To show $\EXP$-hardness, we use $\APSPACE=\EXP$ and present a polynomial reduction from alternating polynomial-space Turing machines to solving games.

Given an alternating PSPACE Turing machine $\A = \zug{Q, \Gamma, \delta, q_0, q_{acc}, q_{rej}}$ and an input word $w$,

we construct a game $\G = \zug{V, E, L, K, \ell, k, T}$ and an initial configuration $\zug{v_0, A}$ such that wins from $\zug{v, A}$ in $\G$ iff $w$ is accepted by $\A$.

Recall that $\A$ uses $m$ tape cells where $m$ is polynomial in the length of the input word $w$.

We simulate configurations using locks.
For each $1 \leq i \leq m$ and $\gamma \in \Gamma$, we introduce a lock $\lock_{i, \gamma}$. Recall that a configuration of $\A$ is $c = \zug{q, \pos, \zug{\gamma_1,\ldots, \gamma_m}}$, meaning that the control state is $q$, the head position is $\pos$, and $\zug{\gamma_1,\ldots, \gamma_m}$ is the tape content. In the configuration in $\G$ that simulates $c$
the only locks that are open are $\lock_{i, \gamma_i}$, for $i \in \set{1,\ldots,m}$.

We describe the vertices and edges in $\G$. The main vertices form the set $Q \times \set{1,\ldots,m} \times \Gamma$.
When the token is placed on $v = \zug{q, \pos, \gamma}$, then the configuration in $\A$ agrees with $v$ in that the control state is $q$, the head position is $\pos$, and the tape content at position $\pos$ is $\gamma$. The owner of $v$ in $\G$ coincides with the owner of $q$ in $\A$. We add intermediate vertices and edges between main vertices.

Outgoing edges from main vertices lead to vertices associated with transitions, and specifically, outgoing edges from $v$ lead to vertices of the form $\zug{v, t}$, for each $t \in \delta(q, \gamma)$. Some “book-keeping” needs to be performed so that the configuration in $\A$ coincides with the configuration in $\G$.
Let $t = \zug{q', \gamma', B}$, and let $\pos'$ be the next position as defined above by $\pos$ and $B$.
For the edge $\zug{v, \zug{v, t}}$, we have $\kappa(\zug{v, \zug{v, t}}) = \{k_{i, \gamma'}, k_{i', \gamma''}\}$, and we turn the keys to close  $\lock_{\pos, \gamma}$ and open $\lock_{\pos, \gamma'}$.
Outgoing edges from $\zug{v, t}$ lead to main vertices having control state $q'$ and head position $\pos'$.
Let the tape content of $\pos'$-th position be $\gamma''$ in the respective configuration of $\A$.
The edge $\zug{\zug{v, t}, \zug{q', \pos', \gamma''}}$ is labeled by the lock $\lock_{\pos', \gamma''}$ which is open.
The next main vertex of $\G$ is thus $\zug{q', i', \gamma''}$.

Note that only $\lock_{\pos', \gamma''}$ is open, while all locks $\lock_{\pos', \widehat{\gamma}}$ for $\widehat{\gamma} \neq \gamma''$ are closed.

Each intermediate vertex $\zug{v, t}$ leads to an intermediate vertex $u$. Let $t = \zug{q', \gamma', B}$ and let $\pos'$ be the next position as defined above by $\pos$ and $B$. On the edge $\zug{\zug{v, t}, u}$ we turn the keys to close  $\lock_{\pos, \gamma}$ and open $\lock_{\pos, \gamma'}$. Outgoing edges from $u$ lead to main vertices having control state $q'$ and head position $\pos'$. The edge $\zug{u, \zug{q', \pos', \gamma''}}$ is labeled by the lock $\lock_{\pos', \gamma''}$. Since only one lock is open for each position, only one of these edges is enabled.
Hence, it is not hard to verify that there is a one-to-one correspondence between runs of $\A$ and plays of $\G$
Thus forces $\A$ to reach a configuration with control state $q_{acc}$ iff forces to reach a main vertex with control state $q_{acc}$.

Note that $\G$ has $|Q| \cdot m \cdot |\Gamma|$ main vertices. If $\A$ has $n$ transitions, then each main vertex is associated with at most $n$

intermediate vertices. Thus, the construction is clearly polynomial.

$t \in \delta(q, \gamma)$ has $m$ outgoing edges leading to vertices of the form $\zug{t, i}$, for $i \in \set{1,\ldots,m}$. The edge $\zug{t, \zug{t, i}}$ is locked with the lock $\lock_i$ so that only one edge can be traversed. Next, $\zug{t,i}$ has $|\Gamma|$ outgoing edges and edge $\zug{\zug{t, i}, \zug{t, i, \gamma''}}$ is labeled by the lock $\lock_{i, \gamma''}$. Since only one tape content lock is open for each position, only one such edge can be traversed. In our case, the vertex that will be reached is $\zug{t, p, \gamma}$ since $\lock_p$ is the only position lock that is open and $\lock_{p, \gamma}$ is the only tape content lock that is open for position $p$. There is a unique outgoing edge from $\zug{t, p, \gamma}$ to an intermediate vertex $u$ on which we turn keys
to close  $\lock_{p, \gamma}$ and open $\lock_{p, \gamma'}$, and to close $\lock_p$ and open $\lock_{p'}$, where $p'$ is determined according to $p$ and $B$ as above. Finally, outgoing edges from $u$ lead to main vertices having control state $q'$. An edge to $\zug{q', p', \gamma''}$ is labeled by lock $\lock_{p'}$ and $\lock_{p', \gamma''}$. Since only one tape position lock is open and only one tape content lock is open for each position, only one such edge can be traversed.

§.§ Proof of Lem. <ref>

Let $f$ be a winning strategy in $\G$. We describe a winning strategy $f'$ in $\G'$. The proof is dual when wins in $\G$. 's strategy $f'$ simulates the execution of $f$ on $\G$ so that when the token is placed on $v \in V$ in $\G'$ it is also placed on $v$ in $\G$. Moreover, if $v \in V_1$ in $\G$, then controls $v$ in $\G'$.

Initially, the invariant clearly holds. Suppose that is playing $\G'$ according to some strategy $g'$. We show that either $f'$ wins by reaching $t$, or that the invariant is maintained. Suppose that the token is placed on $v \in V$. We distinguish between three cases. (1) If $v \in V_2$ and owns $v$ in $\G'$, then he moves to $t$ to win the game. (2) Suppose that $v \in V_2$, that owns $v$, and that she moves to $u'$.
The simulation in $\G$ proceeds to vertex $u$.
In order to maintain the second part of the invariant, does not grab $u'$ but grabs $u$ when $u \in V_1$, which is possible because in such a case we define $u' \in V'_2$. (3) When $v \in V_1$, the invariant implies that controls $v$ in $\G'$. then copies the move of $f$ in $\G$; namely, let $u = f(v)$, then $u' = f'(v)$. The move from $u'$ is as in case (2).

Let $v_0, v_1,\ldots$ be the play in $\G$. Clearly, if case (1) occurs at some point, wins $\G'$. Assume that it does not occur. Then, the invariant implies that the play in $\G'$ is $v_0, v'_1, v_1, v'_2, v_2,\ldots$. Since $f$ is winning in $\G$, there is an $i \geq 0$ such that $v_i = t$, thus the play is winning in $\G'$ as well.

§.§ Proof of Lem. <ref>

Let $\P^k_O = \set{P \in 2^\P: \set{v^k_{\text{in}}, v^k_1, v^k_4, v^k_5, v^k_6} \cap P = \emptyset \wedge \set{v^k_2, v^k_7, v^k_8} \subseteq P}$ and $\P^k_C = \set{P \in 2^\P: \set{v^k_{\text{in}}, v^k_1, v^k_4, v^k_5, v^k_6} \subseteq P \wedge \set{v^k_2, v^k_7, v^k_8} \cap P = \emptyset}$. Note that $\P^k_O \subseteq \P^\ell_O$ and $\P^k_C \subseteq \P^\ell_C$.

We depict $\G_k$ in two configurations in Fig. <ref>. The vertices $v^k_3$ and $v^k_{\text{out}}$ are controlled by one-vertex pawns. The rest of the vertices in $\G_k$, not including targets, are controlled by three pawns and are depicted using colors. Vertex $v^k_1$ is controlled by a “blue” pawn, who also owns $v^\ell_1$. Vertices $v^k_2$, $v^k_7$, and $v^k_8$ are all owned by a “green” pawn who also controls $v^\ell_2$. The other vertices are owned by a “red” pawn.

We simulate the properties of a key using the configurations, where we prove the claim for an entry configuration in $\P^k_C$ and the proof for $\P^k_O$ is dual. We claim that for $i \in \set{1,2}$, if the token lands on $v^k_2$ when controls that vertex, then loses.
Indeed, following 's move at $v^k_2$, grabs $v^k_3$ and directs the token to the winning vertex.
It follows that

does not grab $v^k_{\text{in}}$ upon entry to $\G_k$ and allows to move. Following 's move at $v^k_{\text{in}}$, grabs $v^k_1$, and proceeds to $v^k_4$.
Since moves and $v^k_4$ is in the control of , no change of pawns occurs. We claim that

now proceeds to $v^k_5$. Indeed, if she proceeds to $v^k_6$, will grab $v^k_6$ and win by moving to $t$.
Observe that grabs the red pawn since it controls $v_5^k$ following 's move from $v^k_4$ to $v^k_5$.
Indeed, otherwise proceeds to $s$ to win the game.
Finally, following 's move from $v^k_5$, must grab the green pawn since it grabs $v_7^k$, otherwise moves from $v^k_7$ to $t$ to win the game.
To conclude, if the token exits $\G_k$, has grabbed the blue and red pawns and has grabbed the green pawn. The configuration upon exiting $\G_k$ is thus in $\P^k_O$, and we are done.

We depict $\G_k$ in two configurations in Fig. <ref>. The vertices $v^k_3$ and $v^k_{\text{out}}$ are controlled by one-vertex pawns. The rest of the vertices in $\G_k$, not including targets, are controlled by three pawns and are depicted using colors. Vertex $v^k_1$ is controlled by a “blue” pawn, who also owns $v^\ell_1$. Vertices $v^k_2$, $v^k_7$, and $v^k_8$ are all owned by a “green” pawn who also controls $v^\ell_2$. The other vertices are owned by a “red” pawn. Again, we simulate the properties of a key using the configurations.
Let $\P^k_O = \set{P \in 2^\P: \set{v^k_{\text{in}}, v^k_1, v^k_4, v^k_5, v^k_6} \cap P = \emptyset \wedge \set{v^k_2, v^k_7, v^k_8} \subseteq P}$ and
$\P^k_C = \set{P \in 2^\P: \set{v^k_{\text{in}}, v^k_1, v^k_4, v^k_5, v^k_6} \subseteq P \wedge \set{v^k_2, v^k_7, v^k_8} \cap P = \emptyset}$ (see Fig. <ref>). Note that $\P^k_O \subseteq \P^\ell_O$ and $\P^k_C \subseteq \P^\ell_C$.

We prove the lemma for an entry configuration in $\P^k_C$ and the proof for $\P^k_O$ is dual.

We claim that for $i \in \set{1,2}$, if the token lands on $v^k_2$ when controls that vertex, then loses. Indeed, following 's move at $v^k_2$, grabs $v^k_3$ and directs the token to the winning vertex.
It follows that

does not grab $v^k_{\text{in}}$ upon entry to $\G_k$ and allows to move. Following 's move at $v^k_{\text{in}}$, grabs $v^k_1$, and proceeds to $v^k_4$.

Since moves and $v^k_4$ is in the control of , no change of pawns occurs. We claim that

now proceeds to $v^k_5$. Indeed, if she proceeds to $v^k_6$, will grab $v^k_6$ and win by moving to $t$.
Observe that grabs the red pawn since it controls $v_5^k$ following 's move from $v^k_4$ to $v^k_5$.
Indeed, otherwise proceeds to $s$ to win the game.
Finally, following 's move from $v^k_5$, must grab the green pawn since it grabs $v_7^k$, otherwise moves from $v^k_7$ to $t$ to win the game.

To conclude, if the token exits $\G_k$, has grabbed the blue and red pawns and has grabbed the green pawn. The configuration upon exiting $\G_k$ is thus in $\P^k_O$, and we are done.

§ MISSING DETAILS AND PROOFS FROM SECTION <REF>

§.§ Description of $\delta$-path

The $\delta$-path shown in Figure <ref> is along a closed key $k_i$, an open key $k_j$ and an open lock $\ell_r$ such that $r\neq i$.
An open key represents that the corresponding lock is currently open, and going through this key closes the lock and also the state of the key changes from open to closed.
Similarly, a closed key represents that the corresponding lock is currently closed, and going through this key opens the lock and also the state of the key changes from closed to open.
Recall from the proof of Thm <ref>, that we go through the open key for lock $\ell_{i, \gamma'}$ and the closed key for lock $\ell_{i, \gamma}$ and finally, the open lock $\ell_{i', \gamma''}$.
For simplicity of notation, here, we refer to the keys corresponding to the locks $\ell_{i, \gamma'}$ and $\ell_{i, \gamma}$ as $k_i$ and $k_j$ respectively, while we denote by $\ell_r$ the lock $\ell_{i', \gamma''}$.
Recall from Section <ref> that the gadget for Key $k_m$ and Lock $\ell_m$ mainly have vertices owned by three pawns $p_{Red_m},p_{Blue_m},p_{Green_m}$.
$p_{Red_m}$ owns vertices $\{v_{in}^{k_m},v_{4}^{k_m},v_{5}^{k_m},v_{6}^{k_m}\}$, pawn  $p_{Blue_m}$ owns $\{v_{1}^{k_m},v_{1}^{l_m}\}$, and pawn $p_{Green_m}$ owns $\{v_{2}^{k_m},v_{7}^{k_m},v_{8}^{k_m},v_{2}^{l_m}\}$.
In this $\delta$-path we have pawns $p_{Red_m},p_{Blue_m},p_{Green_m}$ for $m=i,j,r$(The pawns $p_{Blue_i},p_{Blue_j},p_{Blue_r}$ are different pawns even though the vertices owned by them have the same colour in a $\delta$-path and the same holds for vertices belonging to pawns $p_{Red}$ and $p_{Green}$.).
The ownership of the diamond vertices is not fixed; they can be either controlled by or .

[node distance=9mm, main/.style = draw,circle, text=black, inner sep=1pt,gain/.style = draw,square, text=black, inner sep=1pt,main1/.style = draw,circle, blue, left color=blue!20, text=black, inner sep=1pt,main2/.style = draw,circle, red, left color=red!20, text=black, inner sep=1pt,main3/.style = draw,circle, green, left color=green!20, text=black, inner sep=1pt,gain1/.style = draw,square, blue, left color=blue!20, text=black, inner sep=1pt,gain2/.style = draw,square, red, left color=red!20, text=black, inner sep=1pt,gain3/.style = draw,square, green, left color=green!20, text=black, inner sep=1pt,gain/.style = draw,square, text=black, inner sep=1pt,pain/.style = draw,diamond, text=black, inner sep=1pt]
[main2] (1) $v^{k_i}_{\text{in}}$;
[main1] (2) [right of=1] $v^{k_i}_1$;
[gain3] (3) [below of=2] $v^{k_i}_2$;
[pain] (4) [left of=3] $v^{k_i}_3$;
[pain] (5) [below right of=4] $s$;
[accepting,pain] (6) [below left of=4] $t$;
[main2] (7) [right of=2] $v^{k_i}_4$;
[main2] (8) [above right of=7] $v^{k_i}_5$;
[main2] (9) [below right of=7] $v^{k_i}_6$;
[gain3] (10) [right of=8] $v^{k_i}_7$;
[gain3] (11) [right of=9] $v^{k_i}_8$;
[pain] (12) [below right of=10] $v^{k_i}_{\text{out}}$;
[accepting,pain] (13) [right of=10] $t$;
[pain] (14) [right of=11] $s$;
[pain] (15) [left of=8] $s$;
[accepting,pain] (16) [left of=9] $t$;
[gain2] (111) [right of=12]$v^{k_j}_{\text{in}}$;
[gain1] (112) [right of=111] $v^{k_j}_1$;
[main3] (113) [below of=112] $v^{k_j}_2$;
[pain] (114) [left of=113] $v^{k_j}_3$;
[pain] (115) [below right of=114] $s$;
[accepting,pain] (116) [below left of=114] $t$;
[gain2] (117) [right of=112] $v^{k_j}_4$;
[gain2] (118) [above right of=117] $v^{k_j}_5$;
[gain2] (119) [below right of=117] $v^{k_j}_6$;
[main3] (1110) [right of=118] $v^{k_j}_7$;
[main3] (1111) [right of=119] $v^{k_j}_8$;
[pain] (1112) [below right of=1110] $v^{k_j}_{\text{out}}$;
[accepting,pain] (1113) [right of=1110] $t$;
[pain] (1114) [right of=1111] $s$;
[pain] (1115) [left of=118] $s$;
[accepting,pain] (1116) [left of=119] $t$;
[pain] (20) [right of=1112] $u$;
[pain] (31) [left of=1] $v$;
[pain] (32) [left of=31] $v'$;

[pain] (21) [right of=20]$v^{\ell_r}_{\text{in}}$;
[gain1] (22) [above right of=21] $v^{\ell_r}_1$;
[main3] (23) [below right of=21] $v^{\ell_r}_2$;
[pain] (24) [right of=22] $v^{\ell_r}_3$;
[pain] (25) [right of=23] $v^{\ell_r}_4$;
[pain] (26) [below right of=24] $v^{\ell_r}_{\text{out}}$;
[main] (27) [right of=24] $s$;
[main,accepting] (28) [right of=25] $t$;
[pain] (30) [right of=26] $u'$;
[pain] (33) [right of=30] $v_2'$;
[->] (30) – (33);
[->] (20) – (21);
[->] (26) – (30);
[->] (21) – (22);
[->] (21) – (23);
[->] (22) – (24);
[->] (23) – (25);
[->] (24) – (26);
[->] (25) – (26);
[->] (24) – (27);
[->] (25) – (28);
[->] (1112) – (20);
[->] (12) – (111);
[->] (31) – (1);
[->] (32) – (31);
[->] (111) – (112);
[->] (112) – (113);
[->] (113) – (114);
[->] (114) – (115);
[->] (114) – (116);
[->] (112) – (117);
[->] (117) – (118);
[->] (117) – (119);
[->] (118) – (1110);
[->] (119) – (1111);
[->] (1110) – (1112);
[->] (1111) – (1112);
[->] (1110) – (1113);
[->] (1111) – (1114);
[->] (118) – (1115);
[->] (119) – (1116);
[->] (1) – (2);
[->] (2) – (3);
[->] (3) – (4);
[->] (4) – (5);
[->] (4) – (6);
[->] (2) – (7);
[->] (7) – (8);
[->] (7) – (9);
[->] (8) – (10);
[->] (9) – (11);
[->] (10) – (12);
[->] (11) – (12);
[->] (10) – (13);
[->] (11) – (14);
[->] (8) – (15);
[->] (9) – (16);

A $\delta$-path is a path between two primed main vertices in an optional- or always-grabbing game, and it crosses two key gadgets and one lock gadget.

[node distance=12mm, main/.style = draw,circle, text=black, inner sep=1pt,gain/.style = draw,square, text=black, inner sep=1pt,main1/.style = draw,circle, blue, left color=blue!20, text=black, inner sep=1pt,main2/.style = draw,circle, red, left color=red!20, text=black, inner sep=1pt,main3/.style = draw,circle, green, left color=green!20, text=black, inner sep=1pt,gain1/.style = draw,square, blue, left color=blue!20, text=black, inner sep=1pt,gain2/.style = draw,square, red, left color=red!20, text=black, inner sep=1pt,gain3/.style = draw,square, green, left color=green!20, text=black, inner sep=1pt,pain/.style = draw,diamond, text=black, inner sep=1pt]
[pain] (20) $u$;
[pain] (21) [right of=20]$v^{\ell_r}_{\text{in}}$;
[gain1] (22) [above right of=21] $v^{\ell_r}_1$;
[main3] (23) [below right of=21] $v^{\ell_r}_2$;
[pain] (24) [right of=22] $v^{\ell_r}_3$;
[pain] (25) [right of=23] $v^{\ell_r}_4$;
[pain] (26) [below right of=24] $v^{\ell_r}_{\text{out}}$;
[main] (27) [right of=24] $s$;
[main,accepting] (28) [right of=25] $t$;
[pain] (30) [right of=26] $u'$;
[pain] (31) [right of=30] $v_2'$;
[->] (30) – (31);
[->] (20) – (21);
[->] (26) – (30);
[->] (21) – (22);
[->] (21) – (23);
[->] (22) – (24);
[->] (23) – (25);
[->] (24) – (26);
[->] (25) – (26);
[->] (24) – (27);
[->] (25) – (28);

Run between two prime main vertices in arena $\Aa''$

§.§ Proof of Lem. <ref>

We will prove this lemma for $i=1$ that is for .
The proof for is similar.
This follows from the fact that in Figure <ref>, the vertices controlled initially by in Key $k_i$ have their corresponding vertices in Key $k_j$ that are initially controlled by .
Further, the gadget for the Lock $\ell_r$ is symmetric for both players.

In order to prove the lemma we first prove some claims.
Note that in all these claims, we talk about a particular player controlling a vertex, for example, in Claim <ref>, we say that controls $v_{1}^{l_r}$, because can ensure that the game reaches such configuration from vertex $v'$.

We can indeed show that has a strategy such that in the $\delta$-path, controls vertex $v_{1}^{l_r}$ when the token reaches this vertex.
Refer to Figure <ref> in the following claims.

If controls vertex $v_{1}^{l_r}$ then has a strategy from $v_{1}^{l_r}$ to reach $v_2'$ which ensures that out of the 4 rounds that moves the token to $v_2'$, he moves the token in at least 2 rounds.

Suppose the token is at vertex $v_{1}^{l_r}$ and controls $v_{1}^{l_r}$.
Then moves the token from $v_{1}^{l_r}$ to $v_{3}^{l_r}$.
can now grab a pawn.
If controls vertex  $v_{3}^{l_r}$, grabs the pawn owning this vertex else he chooses to not grab a pawn.
Note that under both the cases by the end of this round controls vertex $v_{3}^{l_r}$. He now moves the token to $v_{out}^{l_r}$.
Note that till now has moved the token in one round.
Now by the end of this round there are two possible cases:

*  controls $v_{out}^{l_r}$. In this case moves the token to $u'$, and thus it has moved the token in two rounds, and hence regardless of what happens in next round the claim holds.

*  controls $v_{out}^{l_r}$. In this case moves the token to $u'$ and now can control $u'$ and move the token to $v_2'$, which will be his second instance of moving the token and thus the claim holds.

Hence showed.

If controls vertex $v_{2}^{l_r}$ then he has a strategy from $v_{2}^{l_r}$ to reach $v_2'$ which ensures that, out of the 4 rounds that moves the token from $v_2^{l_r}$ to $v_2'$, he moves the token in at least 2 rounds.

Suppose the token is at vertex $v_{2}^{l_r}$ and controls $v_{2}^{l_r}$.
Then moves the token from $v_{2}^{l_r}$ to $v_{4}^{l_r}$.
Now if has the pawn owning vertex $v_{4}^{l_r}$, then is forced to grab this pawn in this round. Thus by the end of this round controls $v_{4}^{l_r}$.
Now moves the token from $v_{4}^{l_r}$ to $v_{out}^{l_r}$.
now can grab a pawn. If controls vertex  $v_{out}^{l_r}$, grabs the pawn owning this vertex else he chooses to not grab a pawn.
Note under both the cases by the end of this round controls vertex $v_{out}^{l_r}$. He now moves the token to $u'$, which will be his second instance of moving the token and thus the claim holds.

If controls vertex $v_{out}^{k_j}$ then he has a strategy from $v_{out}^{k_j}$ to reach $v_2'$ which ensures that, out of the 7 rounds that moves the token from $v_{out}^{k_j}$ to $v_2'$ he moves the token in at least 4 rounds.

Suppose the token is at vertex $v_{out}^{k_j}$ and controls $v_{out}^{k_j}$.
Then moves the token from $v_{out}^{k_j}$ to $u$.
Now by the end of this round there are two possible cases:

*  controls $u$. In this case moves the token to $v_{in}^{l_r}$.
Note that till now has moved the token in two rounds. Now again by the end of this round there are two possible cases:

*  controls $v_{in}^{l_r}$. In this case moves the token to $v_1^{l_r}$. Now note that the token is at vertex $v_1^{l_r}$ and controls $v_1^{l_r}$. Thus by Claim <ref> we know that from here moves the token in at least 2 rounds before reaching $v_2'$.
As till now when the token is at $v_1^{l_r}$ has moved the token in three rounds, thus overall under this case moves the token in at least 5 rounds.

*  controls $v_{in}^{l_r}$. In this case either moves the token to the vertex $v_{1}^{l_r}$ in which case chooses to not grab.
Now note that the token is at vertex $v_1^{l_r}$ and controls $v_1^{l_r}$. Thus by Claim <ref> we know that from here moves the token in at least 2 rounds before reaching $v_2'$.
Otherwise suppose from $v_{in}^{l_r}$ moves the token to vertex $v_{2}^{l_r}$, in which case chooses to not grab.
Now note that here the token is at vertex $v_2^{l_r}$ and controls $v_2^{l_r}$. Thus by Claim <ref> we know that from here moves the token in at least 2 rounds before reaching $v_2'$.
Thus in this case from $v_{in}^{l_r}$ moves the token in at least two rounds.
As till reaching $v_{in}^{l_r}$ has moved the token in two rounds, thus overall under this case moves the token in at least 4 rounds as the token reaches $v_2'$.

*  controls $u$. In this case moves the token to $v_{in}^{l_r}$.
now can grab a pawn. If controls the vertex  $v_{in}^{l_r}$, grabs the pawn owning this vertex else he choose to not grab a pawn.
Note under both the cases by the end of this round controls vertex $v_{in}^{l_r}$.
He now moves the token to $v_1^{l_r}$. Now note that the token is at vertex $v_1^{l_r}$ and controls $v_1^{l_r}$ thus by Claim <ref> we know that from here moves the token in at least two rounds before reaching $v_2'$.
As till reaching $v_1^{l_r}$ has moved the token in two rounds, thus overall under this case moves the token in at least 4 rounds.

Hence showed.

If controls vertex $v_{in}^{k_j}$, then has a strategy from $v_{in}^{k_j}$ to reach $v_2'$ which ensures that, out of the 12 rounds that moves the token from $v_{in}^{k_j}$ to $v_2'$ he moves the token in at least 6 rounds.

Suppose the token is at vertex $v_{in}^{k_j}$ and controls $v_{in}^{k_j}$.
Then moves the token from $v_{in}^{k_j}$ to $v_1^{k_j}$. In this round grabs pawn $p_{Blue_j}$ inorder to control $v_1^{k_j}$.
Now controls $v_1^{k_j}$, he moves the token to vertex $v^{k_j}_4$.
In the next round moves the token from $v^{k_j}_4$ to $v^{k_j}_5$. in this round grabs $p_{Red_j}$ inorder to control $v^{k_j}_5$. Now moves the token from $v^{k_j}_5$ to $v^{k_j}_7$. Here grabs $p_{Green_j}$ inorder to control $v^{k_j}_7$. Now moves the token from $v^{k_j}_7$ to $v^{k_j}_{out}$. now can grab a pawn. If controls vertex  $v^{k_j}_{out}$, grabs the pawn owning this vertex else he choose to not grab a pawn.
Note under both the cases by the end of this round controls vertex $v_{out}^{k_j}$.
Now note that the token is at vertex $v_{out}^{k_j}$ and controls $v_{out}^{k_j}$. Thus by Claim <ref> we know that from here moves the token in at least 4 rounds before reaching $v_2'$.
As till reaching $v_{out}^{k_j}$ has moved the token in two rounds, thus overall under this case moves the token in at least 6 rounds.

If controls vertex $v_{in}^{k_i}$, then he has a strategy from $v_{in}^{k_i}$ to reach $v_2'$ which ensures that, out of the 18 rounds that moves the token to $v_2'$ he moves the token in at least 9 rounds.

controls vertex $v_{in}^{k_i}$, he moves the token to $v_1^{k_i}$, now grabs $p_{Blue_i}$ in order to control $v_1^{k_i}$.
In the next round moves the token to $v_4^{k_i}$. In this round does not grab a pawn.
Now since $p_{Red_i}$ belongs to and $p_{Red_i}$ owns $v_4^{k_i}$, moves the token to $v_6^{k_i}$.
In this round is forced to grab $p_{Red_i}$ in order to control $v_6^{k_i}$.
Now since here controls $v_6^{k_i}$, she moves the token to $v_8^{k_i}$. Now grabs $p_{Green_i}$ and controls $v_8^{k_i}$.
In the next round moves the token to $v_{out}^{k_i}$.
Now observe that till now has moved the token in three rounds.
Now by the end of this round there two possible cases:

*  controls $v_{out}^{k_i}$. In this case moves the token to $v_{in}^{k_j}$, here chooses to not grab a pawn.
Now observe that the token is at vertex $v_{in}^{k_j}$ and controls vertex $v_{in}^{k_j}$ thus by claim <ref> we know that from here moves the token in at least 6 rounds before reaching $v_2'$.
As until reaching $v_{in}^{k_j}$ has moved the token in three rounds, thus overall under this case moves the token in at least 9 rounds.

*  controls $v_{out}^{k_i}$. In this case moves the token to $v_{in}^{k_j}$. Now note that controls $v_{in}^{k_j}$.
Thus the token is at the vertex $v_{in}^{k_j}$ and controls vertex $v_{in}^{k_j}$.
Now by Claim <ref>, we know that from here moves the token in at least 6 rounds before reaching $v_2'$.
As until reaching $v_{in}^{k_j}$ has moved the token in four rounds, thus overall under this case moves the token in at least 10 rounds.

Hence showed.

Now let us prove the lemma.
So the token is at vertex $v'$.
There are two possible cases:

*  controls $v'$. In this case moves the token to  $v$. Now regardless of who controls, $v$ the token reaches $v_{in}^{k_i}$ with controlling vertex $v_{in}^{k_i}$. Note that will not control $v_{in}^{k_i}$ as he would like to control $v_{1}^{k_i}$. As till reaching $v_{in}^{k_i}$ moved the token in atleast one round and by Claim <ref> we know that from here moves the token in at least 9 rounds before reaching $v_2'$, thus overall moves in at least 10 rounds before reaching $v_2'$.

*  control $v'$. In this case moves the token to $v$.
now can grab a pawn.
If controls vertex  $v$, grabs the pawn owning vertex $v$ else he chooses to not grab a pawn.
Note under both the cases by the end of this round controls the vertex $v'$. He now moves the token to $v_{in}^{k_i}$. Again note that will not control $v_{in}^{k_i}$ as he would like to control $v_{1}^{k_i}$.
As until reaching $v_{in}^{k_i}$ moved the token in one round and by Claim <ref> we know that from here moves the token in at least 9 rounds before reaching $v_2'$. Thus overall moves in at least 10 rounds before reaching $v_2'$.

Hence proved.

§.§ Proof of Lem. <ref>

We prove the lemma for .
The case for is analogous.
Suppose has a winning strategy in the optional-grabbing game $\G'$.

Now since for , grabbing an isolated pawn serves no extra purpose than grabbing nothing, the action of not grabbing in the optional-grabbing game can be replaced with grabbing a pawn owning an isolated vertex in the always-grabbing game $\G''$.

Now assuming that has a winning strategy $\sigma_1'$ in the optional-grabbing game $\G'$, consider a winning play $\pi'$ for in $\G'$.
Now assume that in every round in which does not grab a pawn in $\G'$ can be replaced with grabbing a pawn owning an isolated vertex in the always-grabbing game $\G''$.
Thus consider a strategy $\sigma_1''$ of and a strategy of such that in the resulting play grabs a pawn owning an isolated vertex from if in the corresponding round in the optional-grabbing game he does not grab anything, otherwise, $\sigma_1''$ follows the moves of $\sigma_1'$.

Now consider that chooses strategy $\sigma_1''$.
Recall that $\sigma_1'$ is winning for in $\G'$.
We argue that cannot win in $\G''$ against the strategy $\sigma_1''$ of .
Suppose uses a strategy and grabs some pawns owning non-isolated vertices while playing against strategy $\sigma_1''$  of $\PO$ in rounds other than those rounds in $G'$ i which he grabs the pawns owning non-isolated vertices while playing against strategy $\sigma_1'$ of .
Then the resulting play in the always-grabbing game will still be losing for , since otherwise, could have followed the same order of grabbing the non-isolated pawns in the optional-grabbing game $\G'$ and would have won the optional-grabbing game.
This contradicts that $\sigma_1'$ is winning for in the optional-grabbing game.
This implies that if has a winning strategy in the optional-grabbing game $\G'$ from the configuration $\zug{v,P}$, then he has a winning strategy in the always-grabbing game $\G''$ from the configuration $\zug{v, P \cup \{1, \dots, d+10\}}$.

We now only need to show that in every round in $G''$ where moves the token, has an isolated pawn for to grab.
We consider the following claim.

In the always-grabbing game $G''$, for strategy $\sigma_1''$ of and some strategy of , every time the token is at a primed main vertex, that is, at the beginning of a $\delta$-path, owns at least $10$ pawns owning the isolated vertices.

Consider the case in which at a primed main vertex $v$, has $r$ pawns and the token is at $v$.
Now suppose that the token is moved along a $\delta$-path to the next primed main vertex $v'$.
Note that at this next primed vertex $v'$, has at least $r$ pawns.
This clearly holds since by

Corollary <ref>, along the $\delta$-path, $\PO$ grabs at most $10$ pawns and grabs at least 10 pawns.
Thus, after traversing a $\delta$-path, the number of pawns that controls does not decrease.
Now, in a play, every time the token is at a primed main vertex in $\G''$, it goes along a $\delta$-path to reach the next primed main vertex again.
Now the initial vertex is a primed main vertex and has $(d- |P|)+(d+10)$ pawns at the beginning.
Here $P$ is the initial set of pawns owned by in optional-grabbing game $\G'$.
Thus, every time the token reaches a primed main vertex afterwards, $\PT$ has at least $(d- |P|)+(d+10)$ pawns.
Now since there are exactly $d$ non-isolated pawns, and $(d- |P|)+(d+10)\geq (d+10)$, we have that out of the pawns that has at a primed main vertex, at least $10$ are isolated pawns.
Hence proved.

Now to prove Lemma <ref>, since by Corollary <ref>, we know that has a strategy in the always-grabbing game such that from a primed main vertex to reach the next primed main vertex, he needs to grab in at most 10 rounds, and since by Claim <ref>, has at least $10$ pawns owning isolated vertices, whenever the token is at primed main vertex, in every round between primed main vertices where needs to grab, has an isolated pawn that can grab.
Hence by the argument above, if has a winning strategy in the optional-grabbing game $\G'$, we have that also has a winning strategy in the always-grabbing game $\G''$.

Note that the proof of this direction is also analogous for .
We show that if has a winning strategy in $\G'$, then she also has a winning strategy in $\G''$.
In particular, from Corollary <ref>, along a $\delta$-path, grabs in at least $10$ rounds and grabs in at most $10$ rounds.
Also, similar to Claim <ref>, we can show that every time the token is at a primed main vertex, owns at least $10$ pawns owning isolated vertices.
This is because initially, controls $|P|+d+10$ vertices and this invariant is maintained throughout the play whenever the token reaches a primed main vertex.
Now $|P|+d+10 \geq d+10$, and hence, at the beginning of a $\delta$-path, controls at least $10$ pawns owning isolated vertices.

For the converse direction in Lemma <ref>, we use the determinacy argument as follows.
Again, we show the proof for that if wins in the always-grabbing game $\G''$, then he also wins the optional-grabbing game $\G'$.
The proof for is analogous.

Let has a winning strategy in $\G''$.
Then, by determinacy, loses in $\G''$.
Now from Lemma <ref>, by taking the contrapositive for , we have that also loses $\G'$.
Hence, again by determinacy of pawn games, we have that wins $\G'$.

§.§ Proof of Thm. <ref>

Consider a configuration $\zug{v, P}$ of an always-grabbing pawn game $\G$. Let $j \in [d]$ such that $v \in V_j$ and $P' \subseteq P$. Assuming that $j \in P$ implies $j \in P'$, if wins from $\zug{v, P}$, he wins from $\zug{v, P'}$. Assuming that $j \in \overline{P'}$ implies $j \in \overline{P}$, if wins from $\zug{v, P'}$, she wins from $\zug{v, P}$.

We show the case when has a winning strategy.
The case for having a winning strategy is analogous.
Recall from the proof of Thm. <ref> that the cases were argued for both configuration vertices and intermediate vertices.
For configuration vertices, The proof of this theorem is exactly the same as in the proof of Thm. <ref>.
We detail below the case for intermediate vertices in the case of always-grabbing games.
We use the same notations as in the proof of Thm. <ref>.

As in the proof of Thm. <ref>, we again distinguish between two cases: $j \in P$ and $j \notin P$.
Consider an intermediate vertex $\zug{u, c} \in W_{n+1}$.
We will show that $\zug{u, c'} \in W_{n+1}$.
We denote by $\ell$, the pawn that owns $u$.

First consider $j \in P$, thus controls $c$.
We have as in the proof of Thm. <ref> that both $\zug{u, c}$ and $\zug{u, c'}$ are vertices.
Consider a neighbor of $\zug{u, c'}$, a configuration vertex $\zug{u,Q'}$.
Note that in always-grabbing has to grab a pawn $r$ from , thus $Q'=P' \setminus \set{r}$.
There are two cases, either $\ell \in Q'$ or $\ell \notin Q'$.
Recall that in order to apply the induction hypothesis on $\zug{u, Q'}$, we need to find a neighbor $\zug{u, Q}$ of $\zug{u, c}$ such that if $\ell \notin Q'$, then $\ell \notin Q$.
If $\ell \notin Q'$, then we set $Q = P \setminus \{\ell\}$ if $\ell \in P$ and we set $Q = P \setminus \{r\}$ when $\ell \notin P$.
If $\ell \in Q'$, we set $Q = P \setminus \{r\}$.

The rest of the argument is as in the proof of Theorem <ref>.

Next consider the case when $j \notin P$.
In this case, both $\zug{u, c}$ and $\zug{u, c'}$ are vertices.
In always-grabbing, grabs a pawn $r$ in $\zug{u, c}$, thus we have $Q = P \cup \{r\} \supsetneq P$.
We find a neighbor $\zug{u, Q'}$ of $\zug{u, c'}$ to apply the induction hypothesis on.
If $\ell \in P$ and $\ell \in P'$, then we set $Q' = P' \cup \{r\}$.
If $\ell \in P$ and $\ell \notin P'$, then we set $Q' = P' \cup \{\ell\}$.
If $\ell \notin P$ and $\ell \notin P'$, then we set $Q' = P' \cup \{r\}$.
Again, the remaining argument is as in the proof of Theorem <ref> and we are done.

§ PROOFS FROM SECTION <REF>

§.§ Proof of Lem. <ref>

Suppose has a winning strategy in the game $\G$ from configuration $\zug{v,P}$.
We show that has a winning strategy in the game $\G'$ from vertex $\zug{v,i}$.
The other direction of the lemma follows from determinacy of two-player reachability games.
We prove the above for .
The proof for is analogous.

Let $W_j$ be the set of configurations in $\G$ such that has a strategy to reach $T$ in at most $j$ rounds.
Let $A_j$ be the set of vertices in $\G'$ such that has a strategy to reach $T'$ in at most $j$ rounds. We prove the following claim.

If $\zug{v,P} \in W_j$, with () controlling $v$ then $\zug{v, 1}$ ($\zug{v, 2}$) belongs to $A_{2j}$.

We prove this by induction on $j$. For the base case with $j=0$. this clearly holds.
Suppose the claim holds for $j=h$, and we now show that the claim holds for $j=h+1$.

Consider a configuration $\zug{v,P} \in W_{h+1}$.
We first look at the case when controls $v$.
We show that $\zug{v, 1} \in A_{2(h+1)}$.
Note that, by definition of $\G$ and $\G'$, both $\zug{v,P}$ and $\zug{v,1}$ are controlled by in $\G$ and $\G'$ respectively.

Since $\zug{v,P} \in W_{h+1}$ and controls vertex $v$, there is a strategy of that takes the token starting from $v$ with pawns $P$ to a target vertex in $T$ in at most $h+1$ steps.
Let under this strategy, moves the token from $v$ to $u$.

Note that $\zug{u, P'}\in W_h$ for all configurations $\zug{u, P'}$ that can reach after grabbing from or giving a pawn after moves the token from $v$ to $u$.
Let $P_u$ be the pawn owning vertex $u$.
Now from Observation <ref>, we know that once moves the token from vertex $v$

to a vertex $u$, then can reach a configuration $\zug{u, P'}$ with $p_u \in P'$ as well $\zug{u, P''}$ with $p_u \notin P''$.
Thus there exist configurations $\zug{u,P'},\zug{u,P''}$ in $W_h$ such that $p_u\in P'$ and $p_u\notin P''$.
Now suppose the token is at vertex $\zug{v,1}$ in $\G'$.
Since $u$ is a neighbour of $v$, by the definition of $\G'$, we have that vertex $\zug{\widehat{u},2}$ is a neighbour of $\zug{u,1}$ in $\G'$.
We show that $\zug{\widehat{u},2}\in A_{2h+1}$.
Recall that vertex $\zug{\widehat{u},2}$ is controlled by and the only neighbours of this vertex are $\zug{u,1}$ and $\zug{u,2}$.
Now if we show that both $\zug{u,1}$ and $\zug{u,2}$ are in $A_{2h}$, then we are done.

Since we know that there exists $\zug{u,P'}$ in $W_h$ such that $p_u\in P'$, by the induction hypothesis, we have that $\zug{u,1}\in A_{2h}$, and similarly since there exists $\zug{u,P''}$ in $W_h$ such that $p_u\notin P''$, we have that $\zug{u,2}\in A_{2h}$.

The case for which does not control $v$ can also be proved similarly.

Hence showed.

Consider a configuration $\zug{v,P}$ in $\G$ such that the pawn $p_v$ owning $v$ does not belong to $P$.

has a winning strategy from $\zug{v,P}$ in $\G$ iff has a winning strategy from $\zug{v,3-i}$ in $\G'$ for $i \in \{1,2\}$.

Let $\game=(A,\Phi)$ be a given Grab or Give pawn game, where A=$\{\{ v_1,v_2,\dots,v_n\},(V_1,V_2,\dots,V_k),E\}$ and $\Phi=Reach(T)$.
The initial vertex is $v_1$.

Now consider an edge game $\game'=\zug{G',\Phi'}$, where  $G'=(V',E')$ and the objective  $\Phi'=Reach(T')$.
controls vertex set $V'_1$ and controls  vertex set $V'_2=V'$\$V'_1$.
Here $V'=\{v_i^1,v_i^2,u_i^1,u_i^2$ $|\forall 1\leq i\leq n\}$, $V'_1=\{v^1_i,u^1_i\ |\ \forall 1\leq i \leq n\}$, $V'_2=\{v^2_i,u^2_i\ |\  1\leq i \leq n\}$, $E'=\{(v_i^2,u_j^1),(v_i^1,u_j^2)\ |\ \forall (v_i,v_j)\in E\}\cup \{(u_i^1,v_i^1),(u_i^1,v_i^2),(u_i^2,v_i^1),(u_i^2,v_i^2)\ |\ \forall1\leq i\leq n\}$, $T'=\{v_i^1,v_i^2\ | \forall v_i\in T\}$.
The initial vertex is $v_1^1$ if controls $v_1$ in the initial configuration of game $\game$ else the initial vertex is $v_1^2$.
let us assume controls $v_1$ in the initial configuration of game $\game$. Proof will follow similarly for controlling $v_1$.

Player $t$ has a winning strategy in game $\game$ iff Player $t$ has a winning strategy in game $\game'$.

Let us Prove the claim in $\Longrightarrow$ direction i.e. if Player $t$ has a winning strategy in game $\game'$ then Player $t$ has a winning strategy in game $\game$

First let us prove it for $t=1$.
Let $\tau_1:V'_1\longrightarrow V'$ be winning strategy for Player $1$ in game $\game'$.
Now consider the strategy $(\sigma_1,\Bar{\sigma_1})$ for Player $1$ in game $\game$.
The map $\sigma_1:V\longrightarrow V$ is such that  $\sigma_1(v_i)=v_j$ where j is subscript of vertex $\tau_1(v_i^1)$.
The map $\Bar{\sigma_1}:V\longrightarrow\{1,2\}$ is such that $\Bar{\sigma_1}(v_i)=1$ if $\tau_1(u_i^1)=v_i^1$ else it is equal to 2.

$(\sigma_1,\Bar{\sigma_1})$ is winning strategy for Player $1$ in game $\game$.

What we want to show here is $outcome(\game,(\sigma_1,\Bar{\sigma_1}),(\sigma_{2},\Bar{\sigma}_{2}))\in\Phi=Reach(T)$ for all the strategies $(\sigma_{2},\Bar{\sigma}_{2})$ of .
Let $(\sigma_2,\Bar{\sigma}_2)$ be any strategy for in game $\game$. Now consider the strategy $\tau_2$ for in game $\game'$, where $\tau_2:V'_2\longrightarrow V'$ such that  $\tau_2(v_i^2)=u_j^1$ where j is subscript of vertex $\sigma_2(v_i)$ and  $\tau_2(u_i^2)=v_i^{1}$ if $\Bar{\sigma}_2(v_i)=1$ else it is $v_i^2$.

Observe that $outcome(\game',\tau_1,\tau_2)$ is of the form $v_1^1u_{i_1}^2v_{i_1}^{t_1}u_{i_2}^{3-t_1}v_{i_2}^{t_2}\dots u_{i_r}^{3-t_{r-1}}v_{i_r}^{t_r}\dots$ where
\begin{equation}
\label {eq1}
\end{equation}

\begin{equation}
\label {eq2}
\end{equation}

and for all $r\geq0$

\begin{equation}
\label {eq3}
\end{equation}

\begin{equation}
\label {eq4}
\end{equation}

When in game $\game$ plays with strategy $(\sigma_1,\Bar{\sigma_1})$ and plays with strategy $(\sigma_2,\Bar{\sigma_2})$, by the end of $n^{th}$ round the token is at $v_{i_n}$ and vertex $v_{i_n}$ is controlled by Player $t_n$.

We will prove this claim using induction.
Base case for n=1 game starts at $v_1$ and controls vertex $v_1$.
He moves the token to $\sigma_1(v_1)=v_j$ where $j$ is subscript of  $\tau_1(v_1^1)$, by (<ref>) $\tau_1(v_1^1)=u_{i_1}^2$ and thus $j=i_1$.
Now ensures that Player $\bar{\sigma_2}(v_{i_1})$ controls vertex $v_{i_1}$.
By (<ref>) $\tau_2(u_{i_1}^2)=v_{i_1}^{t_1}$ which implies $\bar{\sigma_2}(v_{i_1})=t_1$.
Thus by the end of $1^{st}$ round token is at vertex $v_{i_1}$ and  vertex $v_{i_1}$ is controlled by Player $t_1$.
Now assume that by the end of ${n-1}^{th}$ round token is at vertex $v_{i_{n-1}}$ and vertex $v_{i_{n-1}}$ is controlled by Player $t_{n-1}$.
So in $n^{th}$ round Player $t_{n-1}$ moves the token to  $\sigma_{t_{n-1}}(v_{i_{n-1}})=v_j$ where $j$ is subscript of vertex $\tau_{t_{n-1}}(v_{i_{n-1}}^{t_{n-1}})$, by (<ref>) $\tau_{t_{n-1}}(v_{i_{n-1}}^{t_{n-1}})=u_{i_n}^{3-t_{n-1}}$ and thus $j=i_n$.
Now Player $3-t_{n-1}$ ensures that Player $\bar{\sigma}_{3-t_{n-1}}(v_{i_n})$ controls vertex $v_{i_n}$.
By (<ref>) $\tau_{3-t_{n-1}}(u_{i_n}^{3-t_{n-1}})=v_{i_n}^{t_n}$ which implies $\bar{\sigma}_{3-t_{n-1}}(v_{i_n})=t_n$(look how we defined $\bar{\sigma_t}$ using $\tau_t$).
Thus by the end of $n^{th}$ round token is at vertex $v_{i_n}$ and  vertex $v_{i_n}$ is controlled by Player $t_n$.

Using above claim it is easy to see that  $outcome(\game,(\sigma_1,\Bar{\sigma_1}),(\sigma_2,\Bar{\sigma_2}))=v_1v_{i_1}v_{i_2}\dots$.
Thus if $v_{i_r}^{t_r}$ is visited in $outcome(\game',\tau_1,\tau_2)$ then $v_{i_r}$ is visited in $outcome(\game,(\sigma_1,\Bar{\sigma_1}),(\sigma_2,\Bar{\sigma_2}))$.
As $\tau_1$ is winning strategy for Player $1$ in $\game'$ $outcome(\game',\tau_1,\tau_2)\in Reach(T')$, which means $\exists \  l\geq 1$ s.t. $v_{i_l}^{t_{l}}\in T'$ and is visited in the run $outcome(\tau_1,\tau_2)$.
Thus $v_{i_l}$ is visited in $outcome(\game,(\sigma_1,\Bar{\sigma_1}),(\sigma_2,\Bar{\sigma}_2))$ and belongs to  $T$ (Note $T'=\{v_i^1,v_i^2\ |\ \forall v_i\in T\}$).
Hence $outcome((\sigma_1,\Bar{\sigma_1}),(\sigma_2,\Bar{\sigma_2}))\in Reach(T)=\Phi$.

We showed this for for proof will be similar except in the last paragraph,
we say as $\tau_2$ is winning strategy for Player $2$ in $\game'$ $outcome(\tau_1,\tau_2)\notin Reach(T')$ and thus $outcome((\sigma_1,\Bar{\sigma_1}),(\sigma_2,\Bar{\sigma_2}))\notin Reach(T)=\Phi$ which is easy to see why.

Now let us prove the other direction of the claim, i.e. if Player $t$ has a winning strategy in game $\game$ then Player $t$ has a winning strategy in game $\game'$.

Proof by contradiction.
Suppose if Player $t$ has winning strategy in $\game$ then Player $3-t$ has a winning strategy in game $\game'$ i.e. if Player $3-t$ does not have a winning strategy in game $\game$ then Player $3-t$ has a winning strategy in game $\game'$.
But by $\Longrightarrow$ if Player $3-t$ has a winning strategy in game $\game'$ then Player $3-t$ has a winning strategy in $\game$. Contradiction thus if Player $t$ has a winning strategy in game $\game$ then Player $t$ has a winning strategy in game $\game'$.

§ PROOFS FROM SECTION <REF>

§.§ Proof of Thm. <ref>

Intuitively, we show that a vertex $u \notin W^1_\ell$ has $\eta(u) = \ell+1$ iff can force the game from configuration $\zug{u, P_0}$ to a vertex in $B_\ell$ without making any grabs and in a non-trivial manner. We compute $W^1_{\ell+1}$ as follows. Consider the turn-based game $\G_\ell = \zug{V, E, B_\ell \cup W^1_\ell}$ with $V_1 = P_0$. We say that wins non-trivially from $u \in V$ if he has a strategy $f$ that guarantees the following against any strategy: the resulting play is of the form $u=v_0, v_1, v_2,\ldots, v_m$ with $v_m \in (B_\ell \cup W^1_\ell)$ and it is non-trivial, meaning that $m \geq 1$. Note the difference from standard turn-based games: a target vertex $u \in B_\ell \cup W^1_\ell$ might be losing for when considering winning non trivially, e.g., when $u$ has an outgoing edge to a sink, no non-trivial play that starts in $u$ ends in a target vertex.

Let $U^1_\ell$ denote the set of vertices from which wins in $\G_\ell$ non-trivially. We describe an algorithm for finding $U^1_\ell$.
We construct a game $\G'_\ell$ in which we make a copy $u'$ of each vertex $u \in B_\ell$, and set the neighbors of $u'$ to be $\{v\in N(u): v\notin W^1_\ell \}$. Intuitively, if wins from $u'$ in $\G'_\ell$, he can win in $\G_\ell$ from $u$ in a non-trivial manner: since $u'$ is not winning in $\G'_\ell$, must make at least one step before entering $B_\ell$.
Let $U'$ be the winning set for in $\G'_\ell$.
It is not hard to see that $U^1_\ell = \set{u \notin B_\ell: u \in U'} \cup \set{u \in B_\ell: u' \in U'}$.

Let $u \in U^1_\ell$. We claim that if $u\notin W_{\ell}^1$ then $\eta(u) = \ell+1$. First, since $u\notin W_{\ell}^1$, by the induction hypothesis, $\eta(u) \geq \ell+1$. Next, we show that $\eta(u) = \ell+1$ by showing that wins the $(\ell+1)$-grabbing pawn game $\G$ from configuration $\zug{u, P_0}$. initially plays according to a strategy that forces the game to $B_\ell$ non-trivially without grabbing.
Suppose that is playing according to some strategy and the game visits $u'$ before visiting $u'' \in B_\ell$. Then, grabs $u''$, proceeds to $W^1_\ell$, and uses his winning $\ell$-grabbing strategy from there.

Let $u \notin U^1_\ell \cup W^1_\ell$. We claim that $\eta(u) > \ell+1$. Note that in order to reach $W^1_\ell$ and in particular reach $T$, the game must first visit $B_\ell$. Suppose that is following a winning strategy in $\G_\ell$.  Thus, in order to reach $B_\ell$, must grab $u' \notin B_\ell \cup W^1_\ell$. Suppose that the game reaches a configuration $\zug{u'', P_0 \cup \set{u'}}$, where $u'' \in B_\ell$. By the above, $\eta(u'') \geq \ell+1$. That is, any strategy that wins from $u''$ must make at least $\ell+1$ grabs. Hence, in order to win from $u$, makes at least $\ell+2$ grabs.

Let $n = |V|$. Note that $W^1_n = V$. Computing $W^1_{\ell+1}$ from $W^1_\ell$ requires a call to an algorithm that solves a reachability game, which can be done in linear time. Hence, the total running time of the algorithm is polynomial in the size of $\G$.

Let $u \in U^1_\ell$. We claim that $\eta(u) = \ell+1$. First, note that by the induction hypothesis, $\eta(u) \geq \ell+1$. Next, we show that $\eta(u) = \ell+1$ by showing that wins the $(\ell+1)$-grabbing pawn game $\G$ from configuration $\zug{u, P_0}$. initially plays according to a strategy that forces the game to $B_\ell$ non-trivially without grabbing. Suppose that is playing according to some strategy and the game visits $u' \notin B_\ell$ before visiting $u'' \in B_\ell$. Then, following the move to $u''$, grabs $u''$, proceeds to $W^1_\ell$, and uses his winning $\ell$-grabbing strategy from there.

Let $u \notin U^1_\ell \cup W^1_\ell$. We claim that $\eta(u) > \ell+1$. Note that in order to reach $W^1_\ell$ and in particular reach $T$, the game must first visit $B_\ell$. Suppose that is following a winning strategy in $\G_\ell$.  Thus, in order to reach $B_\ell$, must grab $u' \notin B_\ell \cup W^1_\ell$. Suppose that the game reaches a configuration $\zug{u'', P_0 \cup \set{u'}}$, where $u'' \in B_\ell$. By the above, $\eta(u'') = \ell+1$. That is, any strategy that wins from $u''$ must make at least $\ell+1$ grabs. Hence, in order to win from $u$, makes at least $\ell+2$ grabs.

Let $n = |V|$. Note that $W^1_n = V$. Computing $W^1_{\ell+1}$ from $W^1_\ell$ requires a call to an algorithm that solves a reachability game, which can be done in linear time. Hence, the total running time of the algorithm is polynomial in the size of $\G$

A target set $T$, arena $\Aa$, starting vertex $v_1$, atmost grabs $k$ and a vertex set $I_1$ controlled by at the start of the game.
Player that has winning strategy.

$U=\{v_i\in I_1\ |\ \exists v_j\in T,(v_i,v_j)\in E\}\cup\{v_i\in V$\$I_1\ |\ \forall(v_i,v_j)\in E,v_j\in T\}$

$v_1\in U$$\Aa,T\cup U,v_1,I_1,k$
$W=\{v_i\in V\ |\ \exists v_j\in T,(v_i,v_j)\in E$}

$v_1\notin W$$\Aa,T\cup W,v_1,I_1,k-1$*[f](2)$\Aa',T\cup W,v_{n+1},I_1,k-1$*[f](3)
$\Aa'=(\{v_1,\dots,v_{n+1}\},(\{v_1\},\dots,\{v_{n+1}\}),E\cup \Delta)$
$\Delta=\{(v_{n+1},v_j)\ |\ v_j\in T,(v_1,v_j)\in E\}$

A plain algorithm

As for $k$=0 $k$-Grab game is a simple reachability game. Note here computes the winner in a simple  reachability game, whose PTIME algorithm is already know.

Note that the only way to reach T here is via W.
Observe that $W$ is subset of $V$\$I_1$ i.e. vertices in W are controlled by and every vertex in W has an edge that takes the token away form target set.
Thus for to reach $T$ he has to reach $W$ and control the vertex in $W$, and this should be done in at most k grabs.
Now as $v_1\in W$ by lemma 6 this is equivalent to reaching W in at most k-1 grabs.

Here since $v_1\in W$ we can not apply lemma 6. In this case we add a new vertex $v_{n+1}$ and make it initial vertex.
Vertex $v_{n+1}$ is a copy of $v_1$ with no incoming edges and the outgoing edges are same as that of $v_1$ which does not lead to target set.
Such a construction does not affect the course of the game and ensures that in the next recursion $v_{n+1}\notin W$.

Let $k \in \Nat$, an OVPP $k$-grabbing game $\G = \zug{V, E, T}$, and an initial configuration $c = \zug{v_0, P_0}$. The algorithm is recursive.

First, we consider the turn-based game $\G_0 = \zug{V_1, V_2, E, T}$ that is obtained by fixing 's coalition to be $P_0$. That is, $V_1 = \set{v \in V: v \in P_0}$, and $V_2 = V \setminus V_1$. Let $W_0 \subseteq V$ denote 's winning region in $\G_0$, which can be found in polynomial time using a standard algorithm to solve reachability turn-based games. Note that a winning strategy in $\G_0$ from $u \in W_0$ is a winning strategy in $\G$ that makes no grabs. If $v_0 \in W_0$, we answer that wins $\G$ from $c$.

Next, let the border of $W_0$, denoted $B$, be vertices from which $W_0$ can be reached in one step, thus $B = \set{v \in V : N(v) \cap T \neq \emptyset}$.

We make three observations. (1) In order to win, must traverse a vertex in $B$ before reaching $W_0$.
(2) All vertices in $B$ are controlled by , i.e. $B \cap P_0 = \emptyset$. Indeed, if $u \in (B \cap P_0)$, then $u \in W_0$.
(3) Each $u \in B$ neighbors a vertex that is not in W_0.
Otherwise, again, we have $u \in W_0$.

Claim: wins $\G$ from $\zug{v_0, P_0}$ using $k$ grabs iff he can force reaching $B$ non-trivially with $k-1$ grabs.

For one direction, if reaches $u \in B$ non-trivially by grabbing at most $k-1$ times, he wins by grabbing $u$ upon entering $u$, and proceeding to $W_0$
from there. On the other hand, suppose that plays so that if $B$ is reached, then has grabbed $k$ times. Then, upon reaching $u \in B$, cannot grab, and by (2) and (3), can win. .......

In case $v_0 \notin B$, we recursively call the algorithm with target set

but allowing to grab only $k-1$ times.
We conclude by addressing the case in which $v_0 \in B$.

Recall that may grab a pawn from no matter which of the players makes a move, but grabbing occurs only after the token has moved. That is, we can think .... that is, after (s)he chooses an outgoing edge from the vertex in which the token was residing.
If $v_0$ is in $B$ already in the beginning of the game, then 1 may not be able to grab the pawn controlling $v_0$ and thereby move the token to $\attr(T)$.
Now since all vertices in $B$ are controlled by , so is $v_0$.
Since $v_0 \notin \attr(T)$, we have that may move so that the token does not reach $\attr(T)$.
Thus for this case, when $v_0 \in B$ in the beginning of the game, we should not say that wins the game.
To address this, after computing $B$, we add a new vertex $v_0'$ to the graph, and for every edge $(v_0,v) \in E$, we add a new edge $(v_0',v)$.
Note that $v_0' \notin B$ and we make $v_0'$ the starting vertex instead of $v_0$.
wins the game starting from $v_0'$ if the set $B$ can be reached with at most $k-1$ grabs.

For each value of $k$, we have a recursive call to the algorithm and each such call may again call the algorithm recursively $|V|$ times, and each recursive call run in time $O(E)$.

The algorithm is thus in $\PTIME$.

Let T be a target set, $\Aa$ be a game arena, $v_i$ be initial vertex and let $I_1$ be initial vertex set of .
Now if $k=0$, k-Grab game is a turn based  reachability game, and we know turn based reachability game can be solved in polytime.
Now if $v_i\in T$ then clearly has a winning strategy.
Now suppose $k\neq0$ and $v_i\notin T$ then consider set $U$ which contains vertices initially controlled by that has an edge to $T$ and vertices initially controlled by from which all the outgoing edges leads to $T$ formally, set $U=\{u\in I_1\ |\ \exists v\in T,(u,v)\in E\}\cup\{u\in V$\$I_1\ |\ \forall(u,v)\in E,v\in T\}$.
Now if $U$ is not empty then if can reach $U$ then in the next round he can reach $T$.
Thus $T\cup U$ can be considered as a new target set and we can solve this new game.
Else $U$ is empty, in which case consider set $W$ which contains vertices in $V$ that has at least one outgoing edge to $T$ i.e. set $W=\{u\in V\ |\ \exists v\in T,(u,v)\in E\}$.
Observe that all the vertices in $W$ are owned by i.e. $W\subseteq I_2$(If $u\in W$ is owned by then $u$ belong to $U$, but then set $U$ is not empty, contradiction.).
Now there are two possibilities $v_i$ belongs to $W$ or $v_i$ does not belong to $W$.
If $v_i$ does not belong to $W$ then by lemma 10, if can reach vertex $v\in W$ in $k-1$ grabs then he can reach $v$ and control $v$ in $k$ grabs.
Now it is easy to see that if the token is at vertex $v\in W$ and controls the vertex $v$ then he can move the token to target vertex, and since only way to reach T is via W can reach $T$ in $k$ grabs iff he can reach $T\cup W$ in $k-1$ grabs.
Now finally if $v_1\in W$. Note that we cannot apply lemma 10 here.
So in this case we modify game G to game G' where we add a new vertex $v'_{i}$ and make it a initial vertex.
Vertex $v'_{i}$ is a copy of $v_i$ with no incoming edges and the outgoing edges are same as that of $v_1$ which does not lead to a target vertex, formally, if $\Aa=(V,P,E)$ then $\Aa'=(V\cup \{v'_i\},P\cup\{\{v'_i\}\},E\cup \Delta)$ where $\Delta=\{(v'_{i},v)\ |\ v\notin T,(v_i,v)\in E\}$.
Now consider a game played on $\Aa''$ with $v'_i$ as the initial vertex with initially owning vertex set $I_1$ and owning vertex set $I_2\cup \{v'_i\}$ and the target set is same as that of given game.
Since the initial vertex $v'_i$ is never visited twice in any play, does not need to grab it, hence if can reach T from $v_i$ in $k$ grabs then he can reach $T$ from $v'_i$ in $k$ grabs.
Now observe that by this construction the set $U'$ and $W'$ remains unchanged, i.e. $U'$ will be empty and $W'=W$ and since $v_i'\notin W$ thus if can reach $T\cup W$ from $v'_i$ in $k-1$ grabs he can reach $T$ from $v'_i$ in $k$ grabs. Which implies can reach $T$ from $v_i$ in $k$ grabs.

A target set $T$, an arena $\Aa$, a starting vertex $v_0$, maximum number $k \ge 0$ of pawns that can grab, and a vertex set $I_1$ controlled by at the start of the game.
Player that has a winning strategy.

$v_0 \in T$
$k < 0$

$W_1=\{v_i\in (I_1 \cup T)\ |\ \exists v_j\in T,(v_i,v_j)\in E\}\cup\{v_i\in V \setminus (I_1 \cup T) \ |\ \forall(v_i,v_j)\in E,v_j\in T\}$

$v_0\in T \cup W_1$$\Aa,T\cup W_1,v_0,I_1,k$
$B=\{v_i\in V\ |\ \exists v_j\in T,(v_i,v_j)\in E$}

$v_1\notin B$$\Aa,T\cup W,v_1,I_1,k-1$*[f](2)$\Aa'',T\cup B,v'_0,I_1,k-1$  where  *[f](3)
$\Aa''=(\{v_0,\dots,v_0'\},(\{v_0\},\dots,\{v_0'\}),E\cup \Delta)$  and
$\Delta=\{(v_0',v_j)\ |\ v_j\in T,(v_0,v_j)\in E\}$

A $\PTIME$ algorithm for unconstrained OVPP $k$-grabbing

§.§ Proof of Thm. <ref>

[node distance=8mm,initial text = ,main/.style = draw,circle, text=black, inner sep=1pt,main1/.style = draw,circle, blue, left color=blue!20, text=black, inner sep=1pt,main2/.style = draw,circle, red, left color=red!20, text=black, inner sep=1pt,main3/.style = draw,circle, green, left color=green!20, text=black, inner sep=1pt,gain1/.style = draw,square, blue, left color=blue!20, text=black, inner sep=1pt,gain2/.style = draw,square, red, left color=red!20, text=black, inner sep=1pt,gain3/.style = draw,square, green, left color=green!20, text=black, inner sep=1pt]
[main,initial] (1) 1;
[gain1] (2) [above right of=1] $S_1^1$;
[gain2] (3) [below right of=1] $S_2^1$;
[main] (4) [below right of=2] 2;
[gain3] (5) [below right of=4] $S_3^2$;
[gain2] (6) [above right of=4] $S_2^2$;
[main] (7) [above right of=5] $3$;
[gain3] (8) [right of=7] $S_3^3$;
[main,accepting] (9) [right of=8] $t$;
[main] (10) [right of=6] $s$;
[main] (11) [right of=5] $s$;
[->] (1) – (2);
[->] (1) – (3);
[->] (2) – (4);
[->] (3) – (4);
[->] (4) – (5);
[->] (4) – (6);
[->] (6) – (7);
[->] (5) – (7);
[->] (7) – (8);
[->] (2) to [out=90,in=90,looseness=0.5] (10);
[->] (6) – (10);
[->] (3) to [out=270,in=270,looseness=0.5] (11);
[->] (5) – (11);
[->] (8) – (10);
[->] (8) – (9);

Consider the input to SET-COVER $U = [3]$ and $\S = \set{\set{1}, \set{1,2}, \set{2,3}}$.
The figure depicts the output on this input of the reduction in

Thm. <ref>

Given an input $\zug{U, \S, k}$ to SET-COVER, we construct an MVPP $k$-grabbing pawn game $\G = \zug{V, E, T}$ in which grabs (see Fig. <ref>). Intuitively, $\G$  has a “chain-like” structure, and in order to win, must cross the chain. Certain positions in $\G$ corresponds to $i \in U$. Each neighbor of $i$ correspond to a set $S \in \S$ with $i \in S$. Thus, a choice of at $i$ can be thought of as assigning a set in $\S$ that covers $i$. We construct $\G$ so that before moving to a neighbor $S$ of $i$, must grab the pawn that owns $S$.
All vertices that correspond to $S$ are controlled by the same pawn, thus if moves from $i' > i$ to a neighbor that corresponds to $S$, there is no need to grab again. Since is allowed only $k$ grabs, there is a one-to-one correspondence between winning strategies and set covers of size $k$.

We describe the construction of $\G$ formally. Let $V = U \cup (\S \times U) \cup \set{s, t}$. 's target is $t$ and $s$ is a vertex with no path to $t$, thus it can be thought of as a target for . There are $m+1$ pawns. For $j \in [m]$, Pawn $j$ owns all vertices in $\set{\zug{S_j, i}: i \in U}$. Pawn $0$ owns the vertices in $U$. We describe the edges. For $i \in U$, we define $N(i) = \set{\zug{S_j, i}: i \in S_j}$. For $1 \leq i \leq n-1$ and $j \in [m]$, we define $N(\zug{S_j, i}) = \set{i+1, s}$ and $N(\zug{S_j, n}) = \set{t, s}$. That is, if moves from $i$ to its neighbor $S_j$ without controlling Pawn $j$, then will proceed to $s$ and win the game.

We claim that a set cover $\S'$ of size $k$ gives rise to a winning $k$-grabbing strategy. Indeed, by choosing, for each $i \in U$, to move to $S \in \S'$ and grabbing it if it has not been grabbed previously, guarantees that $t$ is reached using at most $k$ grabs. On the other hand, observe a play of a winning $k$-grabbing strategy against a reasonable strategy; namely, a strategy that always moves to $s$ from a neighboring vertex $u$ when controls $u$. Suppose that the set of pawns $\S'$ is grabbed. It is not hard to see that $\S'$ is a set cover of size at most $k$, and we are done.

§.§ Proof of Lem. <ref>

The intuition is similar to Thm. <ref>. We construct $\G$ to have a chain-like structure that must cross in order to win. The chain consists of two parts. In the first part, each position corresponds to a variable $x_i$, for $i \in [n]$. We construct $\G$ so that if $x_i$ is existentially quantified, then controls $x_i$, and if $x_i$ is universally quantified, then controls $x_i$ and cannot win by grabbing it. We associate a move in $x_i$ with an assignment to $x_i$. Technically, $x_i$ has two neighbors $v_i$ and $\neg v_i$, initially at the control of . If the token reaches a neighbor of $x_i$ without grabbing it, then loses the game. is allowed $n$ grabs, thus in order to win, it is necessary for him to grab, for each $i$, one of the neighbors of $x_i$. It follows that a play that crosses the first part of the chain gives rise to an assignment $f$ to $x_1,\ldots, x_n$.

In the second part of $\G$, we verify that $f$ is valid. Each position of $\G$ corresponds to a clause $C_j$, for $j \in [m]$, all of which are at the control of in the initial configuration of $\G$. Note that once the first part of $\G$ is crossed,  is not allowed any more grabs. The idea is that when arriving at $C_j$, for $j \in [m]$, must control $C_j$, otherwise he loses. Recall that in OMVPP, it suffices to control one of the pawns that owns $C_j$ in order to control it. We define the pawns that own $C_j$ as follows. For $i \in [n]$, call $p_i$ the pawn that owns $v_i$ and $\neg p_i$ the pawn that owns $\neg v_i$. Thus, grabbing $p_i$ and $\neg p_i$ respectively corresponds to an assignment that sets $x_i$ to true and false. If $x_i$ appears in $C_j$, then $p_i$ is an owner of $C_j$, and if $\neg x_i$ appears in $C_j$, then $\neg p_i$ is an owner of $C_j$. Thus, controls $C_j$ iff $f(C_j) = \text{true}$. It follows that wins iff $f$ is valid.

Formally, the vertices of $\G$ are $V = \set{s, t} \cup \set{x_i, v_i, \neg v_i: 1 \leq i \leq n} \cup \set{C_j: 1 \leq j \leq m}$.
The target vertex is $t$. The vertex $s$ is a sink vertex that is winning for , i.e., there is no path from $s$ to $t$. The game consists of $2n+2$ pawns. For each $1 \leq i \leq n$, we associate with variable $x_i$ two pawns, which we denote by $p_i$ and $\neg p_i$. Intuitively, we will construct the game such that in order to win, must grab either $p_i$ or $\neg p_i$, and we associate grabbing $p_i$ and $\neg p_i$ with an assignment that sets $x_i$ to true and false, respectively. Formally, if $x_i$ appears in $C_j$, then $p_i$ is an owner of $C_j$, and if $\neg x_i$ appears in $C_j$, then $\neg p_i$ is an owner of $C_j$.
We use $1$ and $2$ to refer to the final two pawns.
Pawn $1$ owns every vertex $x_i$ such that variable $x_i$ is existentially quantified in $\phi$ and Pawn $2$ owns every vertex $x_i$ such that $x_i$ is universally quantified in $\phi$. In the initial configuration, controls only Pawn $1$.

We describe the edges in the game, which has a chain-like structure. The last vertex on the chain is the target $t$, thus must cross the chain in order to win.
We assume that follows a reasonable strategy; namely, a strategy that proceeds to win at $s$ given the option, i.e., when the game reaches a vertex $u$ at her control and that neighbors $s$.
The token is initially placed on $x_0$. For $1 \leq i \leq n$, the neighbors of $x_i$ are $v_i$ and $\neg v_i$. We associate with the choice at $x_i$, an assignment to $x_i$ in the expected manner.
Suppose that the token is placed on $u \in \set{v_i,\neg v_i}$. We require to grab the pawn that owns $u$ by adding an edge from $u$ to $s$. That is, since initially controls the pawn that owns $u$, if does not grab it, will win from  $u$. For $1 \leq i < n$, the neighbor of $v_i$ and $\neg v_i$ is $v_{i+1}$. The neighbor of $v_n$ and $\neg v_n$ is $C_1$.

Suppose that follows a strategy that leads the token to $C_1$. We observe that since Pawn $1$ is controlled by , chooses the assignment of the existentially-quantified variables.
We claim that 's strategy does not grab Pawn $2$, thus chooses the assignment of the universally-quantified variables.
Indeed, since is restricted to grab at most $n$ pawns and must grab either $p_i$ or $\neg p_i$, for each $1 \leq i \leq n$. If he grabs Pawn $2$, then there exists $1 \leq i \leq n$ such that he cannot grab any of $p_i$ or $\neg p_i$, and the game will necessarily reach either $v_i$ or $\neg v_i$ at the control of , from which she wins.

We describe the outgoing edges from clause vertices.
For $1 \leq j <m$, the vertex $C_j$ has two neighbors, $s$ and $C_{j+1}$, and the neighbors of $C_m$ are $s$ and $t$. That is, in order to draw the game to $t$, must cross all clause vertices. Recall that the definition of OMVPP dictates that chooses how to move the token at a vertex $u$ if he controls at least one of the pawns that owns $u$. Thus, a winning strategy must grab, for each $1 \leq j \leq m$, at least one pawn that owns $C_j$. In turn, grabbing a pawn that owns $C_j$ means that the assignment to $x_1,\ldots,x_n$ that arises from the players' strategies satisfies $C_j$. It follows that wins the game iff $\phi$ is true.

§.§ Proof of Lem. <ref>

Consider the turn-based game $\G'$ that corresponds to $\G$. Recall that $c$ is a vertex in $\G'$. Fix a memoryless winning strategy in $\G'$, which exists since $\G'$ is a turn-based reachability game. Consider some strategy and let $\pi$ be the resulting play. We make three observations. (1) Each vertex in $\G'$ is visited at most once by $\pi$. Otherwise, $\pi$ enters a loop, which is losing for . (2) The configurations can be partially ordered: a configuration $(v, P)$ can only be visited before a configuration $(u, P')$, for $P \subseteq P'$. Indeed, the only manner in which control of pawns changes is by grabbing, which only adds pawns to the set that he already controls. (3) If the game starts from $(v, P)$, then it ends in a configuration $(u, P')$ with $|P'| \leq |P| + k$. Indeed, can only grab $k$ times. Combining (1)-(3) implies that $\pi$ visits $T$ within $|V| \cdot (k+1)$ rounds.

§.§ Proof of Thm. <ref>

Claim: OMVPP $k$-grabbing PAWN-GAMES is in $\PSPACE$.

We describe a $\PSPACE$ algorithm for OMVPP $k$-grabbing PAWN-GAMES as follows.

The algorithm explores an unwinding of the configuration graph of the $k$-grabbing pawn game in a depth-first manner.
We call this unwinding of the configuration graph a game tree.
Recall that after each move by a player in the game, chooses to grab a pawn and if is controlling the current vertex, that is, where the token lies, then chooses a successor, otherwise chooses a successor.
A vertex $v$ that is controlled by is an OR-vertex in the game tree in the sense that there should exist a successor of $v$ which accepts.
On the other hand, a vertex $v$ that is controlled by is an AND-vertex in the game tree in the sense that all the successors of $v$ should accept.

Since by Lemma <ref>, if has a winning strategy then he has one such that for all strategies of , he wins in $n \cdot (k+1)$ steps,

it is sufficient to unwind the configuration graph such that the length of a path in the game tree starting from the initial vertex does not exceed $n \cdot (k+1)$.
At any time during exploring the game tree in a depth-first manner, the algorithm stores the path that is being currently traversed from the initial vertex, and the length of the path is thus at most $n \cdot (k+1)$.
In a depth-first traversal, from each vertex, its successors are visited in a particular order.
At each level of the path that has been currently traversed, the algorithm also keeps count of how many successors of the vertex at that level have been visited, and also the depth of the level from the root of the tree.
The latter ensures that the algorithm does not unwind the configuration graph to an extent so that the length of a path in the game tree exceeds $n \cdot (k+1)$.
Since in the configuration graph, there are at most exponentially many vertices of the form $\zug{v, P}$ where $v$ is a vertex of the $k$-grabbing pawn game and $P$ is a set of pawns, at each level, the count of number of successors that have been visited so far can be stored in $\PSPACE$.
Since the number of levels of the current path is bounded by $n \cdot (k+1)$ which is polynomial and each level uses polynomial space, the algorithm is in $\PSPACE$.

* For $i \in \set{1,2}$, if enters $\G_\ell$ when controls pawn set $P^\ell_O$, then he has a strategy such that no matter how responds, either 's objective is satisfied or the game exits $\G_\ell$ with owning $P^\ell_O$. That is, the lock $\ell$ is open and stays open after it is traversed.

* For $i \in \set{1,2}$, if enters $\G_\ell$ when controls pawn set $P^\ell_C$, then has a strategy that guarantees that 's objective is violated. That is, $\ell$ is closed.

* For $i \in \set{1,2}$, if enters $\G_k$ when controls pawn set $P^\ell_O \cup P^k_O$, then for any strategy, either 's objective is satisfied or $\G^k$ is exited when owns $P^\ell_C \cup P^k_C$. That is, the key is turned and Lock $\ell$ is closed. Dually, when controls $P^\ell_C \cup P^k_C$ upon entering $\G_k$, then when exiting $\G_k$, controls $P^\ell_O \cup P^k_O$.

We define the two gadgets formally as follows and the construction is depicted in Figures <ref> and <ref>. yak yak yak.

Properties (1)-(3) hold.

yak yak

We proceed to construct the pawn game $\G'$ and the initial configuration. yak yak this might be done slightly informally. yak yak

wins in $\G$ from $c$ iff wins in $\G'$ from $c'$.

Since the size of $\G'$ is polynomial in the size of $\G$, we conclude with the following theorem.

Deciding whether wins from an initial configuration in an optional-grabbing pawn game is EXPTIME-complete.

A gadget G is a 4-tuple $\zug{V_G,E_G,v_i,v_o}$ where $\zug{V_G,E_G}$ is a graph and $v_i,v_o\in V_G$ are in-vertex and out-vertex respectively. thus when a gadget is added across an edge (u,v) means there is an edge from u to in-vertex and an edge from out-vertex to v
Now suppose we have game graph $\zug{V,E}$ and we now add gadget G along edge $(u,v)\in E$ then the new game graph is $\zug{V\cup V_G,E\cup E_G\cup \{(u,v_i),(v_o,v)\}}$.
this was a simple gadget.
We now define gadget G corresponding to a particular game $\game=\zug{\Aa,\phi}$ Gadget G here is a $\zug{\Aa',\phi',v_i,v_o}$. where
structure of Arena $\Aa'$ is same as that of $\Aa$.
our first task is to design gadgets corresponding to lock and key in optional-grabbing game.
in order to achive this there will 4 diffrent types of gadgets GLO open lock GLC closed lock GKO key to close open lock and GKC key to open closed lock.
following are the thing that we want to achieve with these gadgets when Player i enters GLC he looses the game. when Player i enters GLO he reaches out vertex i.e. passes through the gadget without any trouble.
when player goes along GKO it closes turn gadget GKO to GKC and also turns gadget GLO to GLC.
similarly when a player goes along GKC it turn gadget GKC to GKO and also turns gadget GLC to GLO.
we can think of gadget GLC as following. if any Player decides to enter this gadget he losses the game. i.e. if Player i decides to go along an edge with gadget GLC  he/she ends up in a sink state thus looses. and if he enters GLO he ends up at out-vertex i.e. allowed to pass through . thus any valid strategy for Player i won't allow him/her to move along a GLC gadget, and going along GLO has no consequences, which full fills the objective of a lock.

Now first let us see that figure 4 is closed lock i.e. if Payer i enters this gadget he loses the game now when Payer i moves the token to $GL_1$ then Player -i can control $GL_1$ and move token to $GL_2$ if his objective is seafty or move to $GL_3$ if his/her objective is reachability.
claim is that Player -i wins this game as suppose his objective is safety then when he moves to

[main] (21) [right of=20]$v^\ell_{\text{in}}$;
[gain1] (22) [above right of=21] $v^\ell_1$;
[main3] (23) [below right of=21] $v^\ell_2$;
[main] (24) [right of=22] $v^\ell_3$;
[main] (25) [right of=23] $v^\ell_4$;
[main] (26) [below right of=24] $v^\ell_{\text{out}}$;
[main] (27) [above of=24] $s$;
[main,accepting] (28) [below of=25] $t$;
[->] (21) – (22);
[->] (21) – (23);
[->] (22) – (24);
[->] (23) – (25);
[->] (24) – (26);
[->] (25) – (26);
[->] (24) – (27);
[->] (25) – (28);

Deciding whether wins from an initial configuration in always grabbing pawn game is EXPTIME-complete.

First we show the hardness proof.

Always grabbing game is EXPTIME-Hard
Till now we are successful in constructing an arena on which optional-grabbing game simulates an APSPACE turing machine, let us call this arena $\Aa$.
Now consider a new modified arena $\Aa'$ which is $\Aa$ with four new vertices controlled by four new pawns.
Initially two out of these four pawns belong to and remaining two belong to .
Now we claim that always-grabbing game on $\Aa'$ is equivalent to optional-grabbing game on $\Aa$.

To understand the idea first we need to understand the key difference between always-grabbing game and optional-grabbing game.
In pawn games there are some pawns that would not like to control in order to win.
We call the rest of the pawns as safe pawns for in a sense that it is safe for to have/grab them.

Now in optional-grabbing game, if a Player does not have a particular pawn initially, then he has a choice to not have this pawn throughout the game; however this is not the case in always-grabbing game.
Consider a scenario where all the pawns that has are the ones would not like to have, now in the next round say moves the token. In the always-grabbing game must grab a Pawn, thus (s)he is forced to grab an unwanted pawn, whereas in optional-grabbing game can simply choose not to grab a pawn from .

Now suppose has a winning strategy in the optional-grabbing game, if we could ensure that in every round when moves the token, have a safe pawn for , then this should suffice to show have a winning strategy in always-grabbing game.

Observe that every run in optional-grabbing game on Arena $A'$ is a sequence of some finite path.
Note that game starts at a main vertex.
Recall from theorem 2 that the main vertices are of the form $(q,i,a)$ where $q$ is state, $i$ is tape head position and $a$ is input alphabet.
Also recall that from every main vertex we pass through two keys and a lock to again come back to the new/same main vertex.
This is a finite path(this path is shown in the figure on next page).
Since target set is subset of main vertices, every run is a sequence of such finite paths.
Thus the task of checking if every round gives the winning player a choice to grab something safe, boils down to defining an invariant: Checking for a finite set of rounds that the winning Player have a safe pawn to grab, and finally at the end of the Path to check if the invariant is maintained.

Wlog suppose has a winning strategy in optional-grabbing game. If we show that in every round in always-grabbing game, has a choice to grab a safe pawn, then we are done.

If we start at a main vertex with having two safe pawns for , and go through the two keys and a lock to a new/same main vertex, then in every round along this path(shown in fig), have a safe pawn for , and at the end of this path have two safe pawns for .

Let us prove this claim.
So we start at a main vertex $v'$ with having two safe pawns for .
controls $v'$, she moves the token to $v$.
Now if $v$ is controlled by then grabs pawn controlling vertex $v$, else he can grab one of the safe pawn belonging to , let us call this pawn $P_{s_1}$. We will go with the worst case scenario and assume that owns the pawn controlling $v$, thus grabs $P_{s_1}$.
Note that this is the worst case scenario as wants to exhaust safe pawns for belonging to her.
In the next round , moves the token to $v_{in}^{k_i}$.
Now it is 's turn to grab, let us call the pawn that she grabs $P_{g_1}$.
In the next round moves the token to $v_1^{k_i}$.
Here grabs $P_{Blue_i}$ controlling $v_1^{k_i}$ and moves the token to $v_4^{k_i}$.
Now can grab $P_{g_1}$ which was initially controlled by him thus is safe.
now moves the token to $v_6^{k_i}$.
In this round grabs $P_{Red_i}$ controlling $v_6^{k_i}$ and moves the token to $v_8^{k_i}$.
now grabs $P_{Green_i}$ controlling $v_8^{k_i}$ and moves the token to $v_{out}^{k_i}$.
Now it is 's turn to grab, let us call the pawn that grabs $P_{g_2}$.
Note that in this round can control $v_{out}^{k_i}$, and the claim is in the worst case scenario controls $v_{out}^{k_i}$, as it forces to grab in the next round. Thus we assume controls $v_{out}^{k_i}$.
Now she moves the token to $v_{in}^{k_j}$.
Here can grab back $P_{a2}$.
In the next round, grabs $P_{Blue_j}$ and moves the token to $v^{k_j}_4$.
Let us call the pawn that grabs in this round $P_{a3}$.
Now moves the token to $v^{k_j}_5$, here grabs $P_{Red_j}$ and moves the token to $v^{k_j}_7$, where grabs $P_{Green_j}$ and moves the token to $v^{k_j}_{out}$.
here can ensure control over $v^{k_j}_{out}$ and if necessary can grab back $P_{a3}$(case when already controls $v^{k_j}_{out}$).
Now moves the token to $u$.
Let us call the pawn that grabs in this round $P_{a4}$.
Now moves the token to $v^{l_r}_{in}$.
Here can ensure control over $v^{l_r}_{in}$ and if necessary can grab back pawn $P_{a4}$.
Now moves the token to $v^{l_r}_2$.
Let us call the pawn that grabs in this round $P_{a5}$.
Next moves the token to $v^{l_r}_4$.
Let us call the pawn that grabs in this round $P_{a6}$, we assume that grabs in order to control $v^{l_r}_4$, thus she moves the token to $v^{l_r}_{out}$, where can take back Pawn $P_{a5}$ and control $v^{l_r}_{out}$.
He then moves the token to $u'$.
Let us call the pawn that grabs in this round $P_{a7}$.
Now moves the token to a next main vertex $v'_2$.
In this round can grab to take back $P_{a6}$.

Note in the first round grabbed $P_{S_1}$ one of the initial two safe pawn.
But now has Pawn $P_{a7}$ which is safe for .
Thus at the end of this path and for the start of the next path still have two safe pawns for .
Thus the invariant is maintained.

Now when we start the game at the initial vertex, the two newly added pawns controlled by act as safe pawns for .
Note that they are safe as has a winning strategy in optional-grabbing game without their presence.
Now claim shows every time the token is at a main vertex, has two safe pawns for and if this is the case both the mechanisms lead game to same next main vertex.
Thus reaches target in always-grabbing mechanism iff reaches target in optional-grabbing mechanism.
Hence both the games are equivalent.

Now there are two possibilities either $v'$ is controlled by or it is controlled by .
Let us assume controls $v'$, she moves the token to $v$.
Now if $v$ is controlled by then grabs the pawn controlling vertex $v$, else he can grab one of the safe pawn belonging to . We will go with the worst case scenario and assume that owns the pawn controlling $v$, thus grabs one of the safe pawns belonging to . Let us call this pawn $p_{s_1}$.
Note that this is the worst case scenario as wants to exhaust safe pawns for belonging to her.
In the next round , moves the token to $v_{in}^{k_i}$.
Now it is 's turn to grab, let us call the pawn that she grab $p_{1}$.
Now if we had assumed that controls vertex $v'$ then too in the worst case scenario and would have grabbed one-one pawn each.
So we can assume that grabbed $p_{s_1}$ and call $p_{1}$ the pawn that grabbed.
Thus proof for both the cases will follow similarly from now on.
In the next round moves the token to $v_1^{k_i}$.
Here grabs $p_{Blue_i}$ controlling $v_1^{k_i}$ and moves the token to $v_4^{k_i}$.
Now can grab $p_{1}$ which was initially controlled by him and thus is safe.
now moves the token to $v_6^{k_i}$.
In this round grabs $p_{Red_i}$ controlling $v_6^{k_i}$ and moves the token to $v_8^{k_i}$.
now grabs $p_{Green_i}$ controlling $v_8^{k_i}$ and moves the token to $v_{out}^{k_i}$.
Now it is 's turn to grab, let us call the pawn that grabs $p_{2}$.
Note that in this round can control $v_{out}^{k_i}$, and the claim is in the worst case scenario controls $v_{out}^{k_i}$, as it forces to grab in the next round. Thus we assume controls $v_{out}^{k_i}$.
Now she moves the token to $v_{in}^{k_j}$.
Here can grab back $p_{2}$.
In the next round, grabs $p_{Blue_j}$ and moves the token to $v^{k_j}_4$.
Let us call the pawn that grabs in this round $p_{3}$.
Now moves the token to $v^{k_j}_5$, here grabs $p_{Red_j}$ and moves the token to $v^{k_j}_7$, where grabs $p_{Green_j}$ and moves the token to $v^{k_j}_{out}$.
here can ensure control over $v^{k_j}_{out}$ and if necessary can grab back $p_{3}$(case when already controls $v^{k_j}_{out}$).
Now moves the token to $u$.
Let us call the pawn that grabs in this round $p_{4}$.
Now moves the token to $v^{l_r}_{in}$.
Here can ensure control over $v^{l_r}_{in}$ and if necessary can grab back pawn $p_{4}$.
Now moves the token to $v^{l_r}_2$.
Let us call the pawn that grabs in this round $p_{5}$.
Next moves the token to $v^{l_r}_4$.
Let us call the pawn that grabs in this round $p_{6}$, we assume that grabs to control $v^{l_r}_4$, thus she moves the token to $v^{l_r}_{out}$, where can take back Pawn $p_{5}$ and control $v^{l_r}_{out}$.
He then moves the token to $u'$.
Let us call the pawn that grabs in this round $p_{7}$.
Now moves the token to the next main vertex $v'_2$.
In this round can grab to take back $p_{6}$.

Note in the first round grabbed $p_{S_1}$ one of the initial two safe pawns.
But now has Pawn $p_{7}$ which is safe for .
Thus at the end of this path still has at least two safe pawns for .
Thus the invariant is maintained.

Consider a scenario where the token is placed on a vertex $u$, and let

has a winning strategy $\sigma$ from $u$ with a pawn set $P_{u}^i$.
Also suppose vertex $u$ is controlled by and under the winning strategy moves the token along the edge $(u,v)$.
then grabs pawn $p\in P_u^i$.
Now consider the following two cases.

* Pawn $p$ does not own $v$.

* Pawn $p$ owns only vertex $v$, and every outgoing neighbour of $v$ has exactly one outgoing edge.

Now let pawn $p$ be of one of the types listed above.
Now when the token is at vertex $v$, pawns $P_u^i \setminus \{p\}$ belong to . Clearly has a winning strategy from this configuration.
For the scenario described above, we have the following claim.

Under the winning strategy $\sigma$, the rounds in which chose not to grab a pawn, in such rounds pawn $p$ is a safe pawn for until the play does not visit a vertex owned by $p$.

Now consider case 1 where $p$ does not own $v$.
Now when the token is at vertex $u$ and $P^i_{u}$ is the pawn set of , then by lemma …for $p\in P^i_{u}$, we know that it does not matter if grabs pawn $p$ from or even if grabs back $p$ from until reaching a predecessor of a vertex $w$ owned by $p$ (assuming grabbed $p$ from in one of the rounds in between), since the ownership of $p$ depends on who controls the predecessor vertex of $w$ along the play.