The subject of the seminar,"infinite computations in automata theory",has developed into a very active field with a wide range of applications, including specification of finite state programs, efficient algorithms for program verification, decidability of logical theories, automata theoretic approaches to analysis and topology,and fractal geometry.

The response to the invitations was very positive: 37 scientists from 12 countries participated, which is about the maximum to be housed at Schloss Dagstuhl. The seminar started or refreshed contacts especially between Eastern and Western research groups; it was successful in joining the efforts to solve some of the fundamental problems in the theory, and helped to support promising new developments.

The program of talks is presented in the Dagstuhl-Seminar-Report in five sections

• Automata and infinite sequence
• Automata on infinite traces
• Tree languages, tree automata, and infinite games
• Logical aspects
• Combinatorial aspect

In the first section, contributions on finite automata accepting or generating infinite sequences are collected. This includes new results on classical problems, like the complementation problem for ω-automata (N. Klarlund), the introduction of appropriate syntactic congruences (B. Le Saec), and the extension of sermigroups by infinite products (R.R. Redziejowski). The subject of multiplicities (measures for the range of different computations on given inputs) was addressed in the talks of D. Perrin as well as J. Karhumäki (who applied it to introduce a new way of computing real functions by finite automata). Other contributions were concerned with the class of locally testable ω-languages (Th. Wilke), with relations defined by two tape ω-automata (Ch. Frougny), and with a unified framework for specifying and verifying programs using recursive automata on ω-sequences (L. Staiger).

An interesting application of infinite computations in automata theory is the analysis of concurrent (and usually nonterminating) programs. A well developed theory for modelling concurrency is that of "Mazurkiewicz traces", in which certain partial orders (instead of words) are used as representations of computations. The recent development of a theory combining both features ("automata on infinite traces") was presented in three contributions (by A. Petit, P. Gastin, and V. Diekert).

A central subject of the seminar was the famous result of M.O. Rabin on complementation for finite automata on infinite trees. The special role of Rabin's theorem rests on several facts. First, it makes possible an automata theoretic treatment of logical systems (including proofs of decidability), in particular for monadic second order theories and logics of programs. Secondly, its proof is tightly connected with the existence of winning strategies in "infinite games", a topic which recently attracts much attention in the study of nonterminating reactive systems. A third aspect is the intriguing difficulty of the proof of Rabin's theorem, which has motivated several approaches for simplification. New results in this subject were presented in four lectures during the seminar: by E.A. Emerson, A.W. Mostowski, P.E. Schupp, and S. Zeitman. In an additional evening session Paul Schupp gave a detailed exposition of his proof of Rabin's theorem. Two further contributions treated alternative and refined versions of Rabin tree automaton definability, namely definability of tree properties in fixed point calculi (D. Niwinski) and by restricted acceptance conditions for tree automata (J. Skurczynski).

Since about thirty years, an important application of finite automata has been their use in the study of monadic second-order theories. These and related logical aspects were treated in talks collected in the fourth section below. A.L. Semenov and An. A. Muchnik gave a survey of Russian work on this subject, concerning extensions of Büchi's successor arithmetic and a strengthening of Rabin's decidability result for the monadic theory of the infinite binary tree. B. Courcelle and G. Sénizergues showed results on monadic second-order logic over graphs (in particular, on definable graph transformations, and on graphs determined by automatic groups). Logical definability in connection with limit laws in model theory and with problems of circuit complexity were presented by K. Compton and H. Straubing.

The final section summarizes lectures which are devoted to more combinatorial. questions (in this case not necessarily applied to infinite objects)". The subjects here were decidability and complexity results on tiling pictures with given dominoes (D. Beauquier), the invertibility of automaton definable functions (C. Choffrut), and new schemes for language generation motivated by mechanisms of DNA splicing (T. Head).

The talks were supplemented by lively discussions, joint work in small groups, and three long night sessions: On Tuesday evening, A. Muchnik presented his extension of the Shelah-Stupp Theorem (showing that the tree unraveling of a structure has a decidable monadic theory if the given structure has). On Wednesday, H. Straubing explained his reduction of general first-order definitions of regular word sets to first-order definitions with modulo counting predicates only. P. Schupp presented on Thursday night his proof on simulation of alternating automata by nondeterrninistic tree automata, thus giving a simplified proof of Rabin's theorem.

Summing up, the meeting made possible a very productive exchange of ideas and results; it will stimulate the research of those who participated and already has led to the solution of open problems. The friendly atmosphere in the house, the most efficient work of the secretary team and last not least the perfect kitchen were appreciated very much. In the name of the participants, the organizers would like to thank the staff for their efforts in making the stay at Schloss Dagstuhl so pleasant and fruitful.

Creative Commons BY 3.0 Unported license