[**Edit, June 2, 2013:** At the Nordic Spring School in Logic this year there was a course by Wolfgang Thomas on *Logic, automata and games*. You may be interested in the slides, particularly for part III (Rabin’s tree theorem). Slides and notes for all courses can be downloaded here; the slides for part III can be downloaded here.]

This is a nice result, but you are right that the known proofs are rather elaborate. Below, I just give the briefest of sketches, but it gives a glimpse of the ideas involved. The game theoretic approach is elegant, even if it takes a bit of time to understand the relevant notions.

An excellent reference is the book "The classical decision problem", by Börger, Grädel, and Gurevich (Springer, 1997). You can find the proof in II.7.1.

I lectured on it in Caltech a few centuries ago (2007). If you do not have access to the book, you may want to take a look at homework sets 5 and 6 at this link. There, you will find a sketch of the so called Forgetful Determinacy theorem of Gurevich and Harrington. This is the key technical result. Here, I'll just state it.

(The theorem comes from Gurevich-Harrington, "Trees, automatas, and games". 14th annual ACM Symposium on Theory of Computation, 60-65, 1982. The presentation in the book follows Zeitman, "Unforgettable forgetful determinacy", Journal of Logic and Computation, vol 4, 273-283 (1994).)

**Theorem (Forgetful determinacy for tree automata).** If $A$ is a $\Sigma$-tree automaton and $F$ is a $\Sigma$-tree, one of the players ($A$ or Pathfinder) has a winning strategy in
$\Gamma(A,F)$ that is *forgetful* in the sense that whenever $p$, $q$ are positions from which the winner moves,
$$ LAR(p)=LAR(q), $$
and
$$ \mbox{$Node(p)$-residue of $F=Node(q)$-residue of $F$}, $$
then $f(p)=f(q)$.

(Here, the node of a position is simply the node in the binary tree that is being played. Given a $\Sigma$-tree $F$, the $v$-residue of $F$ is the $\Sigma$-tree $F_v$ coming from $F$ by only considering the tree from $v$ on, that is, $F_v(w)=F(vw)$. I define the other relevant notions below.)

Using this, it is relatively easy to check that the "Emptiness problem" is decidable for tree automata: There is an algorithm that, given a $\Sigma$-automaton $A$, decides whether there is a $\Sigma$-tree that $A$ accepts.

Similarly, but this takes a bit of work and is really the whole point, Forgetful Determinacy implies that there is an algorithm that to each $\Sigma$-automaton $A$ assigns a $\Sigma$-automaton $C$ with the property that $C$ accepts a $\Sigma$-tree iff $A$ rejects it. (This is the "Complementation Theorem".)

Using this, it is a simple matter of induction in formulas to prove decidability, since one can effectively associate to each monadic formula $\phi(X_1,\dots,X_n)$ (of second-order theory with two successors) a $\Sigma$-automaton $A$ for $\Sigma=\{0,1\}^n$, with the property that, for any collections $W_1,\dots,W_n$ of binary words, the automaton $A$ accepts the tree $T$ they define iff $T^2$ satisfies $\phi(W_1,\dots,W_n)$, where $T^2$ is the structure given by the full binary tree with the two successor functions.

Let me briefly review the relevant definitions, following the book closely. I'm just quoting the notes of my younger self, so there may be a bit of irrelevancy, for which I apologize.

Let $MOVE$ be a finite alphabet. An *arena* $A$ is a colored
bipartite multi-digraph in the following sense:

The *vertices* of $A$ are divided into two disjoint sets,
*east* vertices and *west* vertices. There are no *edges*
between east vertices or between west vertices. There may be
*several* edges between an east and a west vertices, or between a
west and an east vertices (so edges have *directions*, which is
why we call the object a digraph, and there may be several edges
between the same vertices, which is why we call it a multi-digraph).

There is a distinguished vertex, the *start vertex*. Every
vertex is *reachable* from the start vertex (i.e., for any $v$
there is a finite sequence $v_0,\dots,v_n$ where $v_0$ is the start
vertex, $v_n=v$ and for each $i\lt n$ there is an edge going from $v_i$
to $v_{i+1}$). Any vertex has at least one outgoing edge.

The edges are labeled by elements of $MOVE$ in such a way that no
two *outgoing* edges from the same vertex have the same label.

There is a finite set $S$ of *colors* that partition the set of
vertices. We denote by $C^s$ the vertices with color $s$.

A **game** on $A$ is played between two players 0 and 1 who
alternate choosing an outgoing edge from the current vertex,
starting from the start vertex. So a play of the game defines an
infinite *path* through $A$ (we allow for the possibility of
revisiting vertices). A *position* $p$ is a finite directed path
through $A$ from the start vertex, so it is uniquely described by a
word in $MOVE^*$, with which we identify $p$. Given a position $p$,
the labels of the edges leading out of the last vertex of $p$ are
the *possible moves* at $p$. A *play* is an $\omega$-sequence
$P\in MOVE^\omega$ such that each initial segment is a position. The set
of plays over $A$ is $PLAY(A)$.

A **graph game** is a triple $\Gamma=(A,\varepsilon,W_\varepsilon)$ where $A$ is an arena,
$\varepsilon\in\{0,1\}$ (denoting the player that goes first) and
$W_\varepsilon$, the *winning set* for player $\varepsilon$, is
a Boolean combination of the sets ${}[C^s]$ where ${}[C^s]$ is the set
of plays that infinitely often pass through a vertex of color $s$.

Player $\varepsilon$ wins a play $P$ of $\Gamma$ iff $P\in
W_\varepsilon$. Otherwise, player $1-\varepsilon$ wins the play $P$.

Notice that if the start vertex is an east (resp., a west) vertex
then, playing $\Gamma$, player $\varepsilon$'s turns to move are
always at east (resp., west) vertices. Call the set of these
vertices $V_{\varepsilon}$ and the set of remaining vertices
$V_{1-\varepsilon}$.

A **forgetful strategy** $f$ for player $\delta\in\{0,1\}$ in
$\Gamma$ is a function $f:V_\delta\to{\mathcal P}(MOVE)$ that to each
$v\in V_\delta$ assigns a non-empty set of possible moves from $v$.
(The strategy is forgetful since it depends only on $v$ and not on
how $v$ was reached.)

The *latest appearance record* $LAR(p)$ of a position $p$ is an
ordering of the colors. We define $LAR$ inductively, with
$LAR(start)$ being an ordering whose last color is that of the start
vertex. If a position $q$ is obtained from a position $p$ by
adjoining an edge to a vertex of color $s$, then $LAR(q)$ is
obtained from $LAR(p)$ by moving $s$ to the last place. The coloring
of an arena $A$ is *forgetful* if any two positions at the same
vertex have the same $LAR$, in which case we can simply talk of the
$LAR$ at a vertex $v$ (rather than at a position $p$ whose last
vertex is $v$).

What one actually shows is the following:

**Theorem (Forgetful determinacy).**
Let $\Gamma=(A,\varepsilon,W_\varepsilon)$ be a graph game with a
forgetful coloring of the arena $A$. Then one of the players has a
forgetful winning strategy in $\Gamma$.

One then uses this result to prove the version I stated earlier. For this, let $\Gamma(A,F)$ be a game on a $\Sigma$-tree $F$ between
a $\Sigma$-tree automaton $A$ and Pathfinder. Define from this a
graph game whose alphabet consists of the states of $A$ and names
for the two directions left and right. (So $A$ starts the game and
chooses a state according to its initial table, Pathfinder responds
by choosing the name of a direction, then $A$ chooses a state, etc.)

All positions $p$ where $A$ makes a move have the same default
color. If $A$ chooses a state $s$ at $p$ then the color of position
$ps$ is $s$. (One needs to check that this coloring is forgetful.)

One then has that either $A$ or Pathfinder has a forgetful
winning strategy in $\Gamma(A,F)$, by "transfering" the strategy that the forgetful determinacy theorem guarantees.

againstclosing. – Andrés Caicedo May 17 '12 at 7:48