Synthesis of Finite-state and Definable Winning Strategies

Alexander Rabinovich
Church's Problem asks for the construction of a procedure which, given a logical specification $\varphi$ on sequence pairs, realizes for any input sequence $I$ an output sequence $O$ such that $(I,O)$ satisfies $\varphi$. McNaughton reduced Church's Problem to a problem about two-player$\omega$-games. B\"uchi and Landweber gave a solution for Monadic Second-Order Logic of Order ($\MLO$) specifications in terms of finite-state strategies. We consider two natural generalizations of the Church problem to countable ordinals: the first...