Infinite games (in the form of Gale-Stewart games) are studied where a play is a sequence of natural numbers chosen by two players in alternation, the winning condition being a subset of the Baire space $\omega^\omega$. We consider such games defined by a natural kind of parity automata over the alphabet $\mathbb{N}$, called $\mathbb{N}$-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. We show that the classical B\"uchi-Landweber Theorem (for finite-state games in the Cantor space $2^\omega$) holds again for the present games: A game defined by a deterministic parity $\mathbb{N}$-MSO-automaton is determined, the winner can be computed, and an $\mathbb{N}$-MSO-transducer realizing a winning strategy for the winner can be constructed. Comment: Updated header on title page. 26 pages, 1 figure

Determinacy of infinite two-player games is a topic of descriptive set theory that has triggered intensive research in theoretical computer science since 1957 when A. Church formulated his "synthesis problem" (regarding the construction of circuits with infinite behavior from logical specifications). In the first part of the lecture we review the fascinating development of the algorithmic theory of infinite games that was started by Church's problem, that enriched automata theory and related fields, and that led to interesting applications in verification and program synthesis. In the second part we turn to the question how to lift this theory from the case of the Cantor space (where a play is a sequence of bits) to the case of the Baire space (where a play is a sequence of natural numbers). While this step does not involve difficulties in classical descriptive set theory, the algorithmic approach raises non-trivial questions since it requires to consider automata that work over infinite alphabets. We present recent results (joint work with B. Brütsch) that provide a solution of Church's synthesis problem in this context, and we point to numerous questions that are still open.

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many (parameterized) synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components. This result is optimal in the following sense: (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.

Formal verification using the model-checking paradigm has to deal with two aspects. The systems models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models, we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components in a Feferman-Vaught like style. This result is optimal in the following sense. (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.

This tutorial surveys selected recent results on the connection between monadic second-order logic and finite automata. As a unifying idea, the role of automata as normal forms of monadic formulas is pursued. In the first part we start from an automata-theoretic interpretation of existential monadic second-order formulas and in this framework explain the monadic quantifier alternation hierarchy over finite graphs. In the second part, infinite models, in particular /spl omega/-words, are considered. We analyze the logical significance of central constructions in /spl omega/-automata theory and sketch new proofs of decidability results in monadic second-order logic.

We show that in monadic second-order logic over finite directed graphs, a strict hierarchy of expressiveness is obtained by increasing the (second-order) quantifier alternation depth of formulas. thus, the "monadic analogue" of the polynomial hierarchy is found to be strict, which solves a problem of Fagin. The proof is based on automata theoretic concepts (rather than Ehrenfeucht-Fraisse games) and starts from a restricted class of graph-like structures, namely finite two-dimensional grids. We investigate monadic second-order definable sets of grids where the width of grids is a function of the height. In this context, the infiniteness of the quantifier alternation hierarchy is witnessed by n-fold exponential functions for increasing n. It is notable that these witness sets of the monadic hierarchy all belong to the complexity class NP, the first level of the polynomial hierarchy.

Monadic (second-order) theories of well-orderings were first studied by Büchi [1], [2], [3] using concepts of automata theory. There it was shown that the monadic theory of ω, the monadic theory of any countable ordinal, and the monadic theory of ω1 are decidable. Expansions of the well-ordering (ω, <) by further relations were considered in [4], [5], [8] and [9], for example. Concerning such expansions, Buchi and Landweber [4] asked whether there is a set P ⊂ ω such that the weak monadic theory of (ω, <, P) is decidable and the (strong) monadic theory of (ω, <, P) is undecidable. In this note we give a negative answer by proving the following general theorem: If α is an ordinal and an n-tuple of subsets of α, then the monadic theory of (α, <, ) is decidable provided the monadic theory of (cf (α), <), i.e. of the cofinality of α, and the bounded monadic theory of (or, <, ) are decidable. (In the bounded monadic theory the second-order variables range only over bounded subsets of α.) Also we show that in the bounded and the (strong) monadic theory of a structure (α, <, ) the same classes of subsets of α are definable. For the proofs we use a result of Shelah [7] and a suitable version of a combinatorial argument which was introduced by Büchi [1] and McNaughton [6] into the study of monadic theories.