I've been reading Rabin's article on decidability in Barwise's text, and I came across Rabin's discussion of the decidability proof of his tree theory: the second-order theory with two successor functions. The text mentions that the proof is hard and very technical owing to many extensions of automata theory, and I was wondering if someone might be able to sketch it out.
Thanks!
[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.
Here is a very sketchy answer, but it should give the first idea of the proof.
Basically, even on words (structures with one successor), you can decide if an MSO (Monadic Second Order) sentence accepts a model by translating the sentence to an equivalent automaton, and then you just need to find an accepting path in this automaton, which is easy.
What Rabin did is develop a model of automaton running on infinite tree, together with a way to translate MSO sentences to equivalent automata. Then, in the same way, deciding if the MSO sentence accepts a model is reduced to finding a "path" (which is generalized to a tree structure in some way) in the equivalent automaton.
