Logical Approaches to Computational Barriers

Long games with a short memory

Speaker:
| Amit Shomrat |

Author(s): |
Amit Shomrat and Alexander Rabinovich |

Slot: |
Array, 15:10-15:30, col. 4 |

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.

websites: Arnold Beckmann | 2006-06-29 |