The game is actually an instance of two-persons Pebble game, as @HendrikJan pointed out, and as such is proven to be $EXPTIME-complete$. The following is a summary based on a proof by Kasai, Adachi and Iwata in SICOMP 8 (4).
For starters, it's pretty obvious that the game is in $EXPTIME$ - we can simply check all the possible games and see if there is winning strategy. To proove it's $EXPTIME-hard$ is a little bit more challenging.
First we need to know the notion of Alternating Turing machines (or ATMs for short). We will further tighten the definition to get so-called standard ATM:
We say an ATM $M$ is standard if
- $M$ has only one work tape with the head initialized to the first cell of the tape,
- if a configuration $C$ of $M$ is existential (universal), then every configuration $C’ \in Next_M(C)$ is universal (existential),
- the initial state is existential and the accepting state is universal, and
- $Next_M(C) = \emptyset$ if and only if $C$ is an accepting configuration.
Where $Next_M(C)$ deontes set of possible configurations after one move starting from configuration $C$
Now there come two important lemmas proven by Chandra, Kozen and Stockmayer in Journal of the ACM 28(1):
Lemma 1
For every $S(n) \geq log (n)$, if $L \in ASPACE(S(n))$, then $L$ is accepted by a standard ATM within space $S(n)$.
Lemma 2
$EXPTIME = APSPACE$
Having those two in mind, we now see that, given a standard ATM $M = (Q, \Sigma, \Gamma, \delta, b, q_1, q_a, U)$ such that only $p(n)$ cells are
available on the work tape for some polynomial $p$ in $n$, and a word $w = w_1 w_2 ... w_n$, we need to construct, in logarythmic space, an instance of pebbles game $G$ such, that $w$ is accepted by $M$ iff. first player has winning strategy in $G$.
In order to do that we will need
set of fields $X$ consisting of
- fields representing the state of working tape ($\{1..p(n)\} \times \Gamma$)
- fields representing current state of machine and it's heads ($Q \times \{1..n\} \times \{1..p(n)\}$)
- fields representing work tape transitions ($Q \times \{1..n\} \times \{1..p(n)\} \times \Gamma^2)$
- three additional fields $s_1, s_2, t$ to ensure that correct player wins the game
Set $R$ of rules that translates $\delta$ into our game:
- For each element of $Q \times \{1..n\} \times \{1..p(n)\}$ if $\delta (q, w_i, a)$ contains $(q', a', (d', d'')), a \neq a'$ then this transition can be encoded with the following rules:
- $([q, i, l], [l, a], [q, i, l, a, a'])$
- $([l, a], [q, i, l, a, a'], [l, a'])$
- $([q, i, l, a, a'], [l, a'], [q, i+d', l+d''])$
- For each element of $Q \times \{1..n\} \times \{1..p(n)\}$ if $\delta (q, w_i, a)$ contains $(q', a, (d', d''))$ we need just one rule:
- $([q, i, l], [l, a], [q, i+d', l+d''])$
- Finally we need to have "game finishers" rules:
- for each $i$ and $l$ there should be rule $([q_a, i, l], s_1, s_2)$
- we also add rule $(s_2, s_1, t)$
And to start the game properly we need the set $S = \{[q_1,1,1],s_1\} \cup \{[l,b] | 1 \leq l \leq p(n)\}$, which denotes that we're in initiall state, both heads are at the beggining of the tapes, and the working tape is empty.
From this, the proof of the fact that $w$ is accepted by $M$ iff. first player has a winning strategy in $G$ should be pretty straightforward.
