Two fundamental results of automata theory are the decidability of the
Monadic second-order Logic of Order (MLO) over $\omega$
and the computability of the Church-synthesis problem over $\omega$.
In their classical paper [BL], Buchi and Landweber reduce the
Church-synthesis problem to $\omega$-length two-person games of
perfect information, where the winning condition is definable by an
MLO-formula (the so called "regular" games).
Their main theorem states:
Theorem (BL): (a) In every such game, one of the player has a
winning straegy,
(b) the winning player has a winning strategy that is definable by
a finite automaton with output, and
(c) there exists an algorithm that, given such a game (that is, a
formula defining the winning condition),
determines which of the two players has a winning strategy and
constructs a finite-automaton defining such
a strategy.
Buchi generalized the concept of an automaton to allow automata to
"work" on a countable ordinal
and used this to show that the MLO-theory of any countable ordinal is
decidable (see [BS]).
BL state that their theorem could also be generalized to all
countable ordinals. However, we show:
Theorem: The BL theorem holds for a countable ordinal $\alpha$
iff $\alpha<\omega^\omega$.
In particular, there is a regular game of length $\omega^\omega$
in which
none of the players has a finite-state strategy.
Our proof uses both game theoretical techniques and the
"compositional method"
associated with the names of Feferman-Vaught, Shelah and others.
We will also discuss the decidability of the Churuch-synthesis
problem over a given countable ordinal
and an exact characterization of games (i.e., formulas) for which the
winning player has a finite-state strategy.
References:
[BS] J. R. Buchi, D. Siefkes, The Monadic Second-order Theory of all
Countable Ordinals, Springer Lecture Notes 328 (1973), pp. 1-126.
[BL] J. R. Buchi, L. H. Landweber, Solving Sequential Conditions by
Finite-State Strtegies, Transactions of the AMS, Vol. 138 (Apr.
1969), pp. 295-311.