Infinite Words: Automata, Semigroups, Logic and Games

Automata theory arose as an interdisciplinary field, with roots in several scientific domains such as pure mathematics, electronics and computer science. This diversity appears in the material presented in this book which covers topics related to computer science, algebra, logic, topology and game theory. The elementary theory of automata allows both the specification and the verification of simple properties of finite sequences of symbols. The possible practical applications include lexical analysis, text processing and sofware verification. There are at least two possible extensions of this theory. The theory of formal series is one of them. Words are replaced by functions associating to each word some numerical value. This value can be an integer counting the number of paths labeled by this word in an automaton or the integer represented by this word in some basis. It can also be a real number corresponding to some probability of the word. The other possible extension is the subject of this book: Finite sequences of symbols are replaced by infinite sequences. The motivation for this generalization originates in the early work of Richard Büchi in the sixties. Working on weak logical theories of the integers, he was lead to consider the monadic second order theory of the successor function on the integers. He was able to prove the decidability of this theory. He actually showed that all properties of the integers expressible in this logic can also be defined in terms of finite automata. Later on, Robert McNaughton proved the equivalence of deterministic and non-deterministic automata, a natural extension of the corresponding result for finite words. This difficult result had been conjectured by David Muller while working at questions related to oscillating circuits. Many other results have appeared since then and the theory has known an important increase of interest motivated by applications to problems in computer science. The notion of an infinite sequence is of interest to model the behavior of systems which are supposed to work endless, as operating systems for example. This book presents a comprehensive treatment of all aspects of this theory. It gathers for the first time the basic results with the advanced ones. Actually, if several surveys have appeared on infinite words, this book is the first manuel devoted to this topic. All proofs are given in detail, with a few, duly mentionned, exceptions. The book is intended for researchers or advanced students in mathematics or computer science. No particular background is required to read it, except for a standard mathematical culture. The dependence between chapters is not too strong, making it possible to read some chapters independently from other ones. The book can be used to lecture and the authors have used the manuscript for several years for graduate courses in computer science. It is unlikely to cover the whole content in one single course, but a selection with emphasis either on topology, or on logic, or on automata and semigroups, is possible. The book is organized as follows. The first chapter contains the definitions of rational expressions, Büchi and Muller automata and recognizable sets. It covers the necessary elements of the theory of automata on finite words such as Kleene's theorem. A proof of McNaughton theorem is given, using Safra's determinization algorithm. Although this construction is rather involved, we have chosen to place it at the very beginning of the book because it is straightforward. Other proofs of McNaughton's theorem are given later on. In the second chapter, we shift to a more algebraic point of view. The key idea of this chapter is to give a purely algebraic definition of recognizable sets. This point of view will be adopted quite often in the sequel. Our main tools are finite semigroups and their counterpart for infinite words, called omega-semigroups. The third chapter introduces the topological aspects of the theory. It is really an excursion in the field known as descriptive set theory, situated at the border between analysis and logic. We show that the main notions introduced so far have a natural translation in terms of topology. The fourth chapter is devoted to games. These games are two player mathematical games which are used as a tool to prove some results on infinite words and automata. For instance, in this chapter, games are used to prove the Büchi-Landweber theorem. Some particular games, such as Wadge games or Fraïssé-Ehrenfeucht games, are used in further chapters. In the fifth chapter, we present a classification of recognizable sets of infinite words known as the Wagner hierarchy. It emphasizes once again the importance of finite semigroups in this theory. Chapters 6 and 7 present the theory of varieties for infinite words. It is an extension of the so-called Eilenberg variety theory, which associates sets of finite words and families of finite semigroups. The families of semigroups are actually varieties of finite semigroups. The extension to infinite words leads to the notion of varieties of omega-semigroups. The classical result of Schützenberger on star-free sets and aperiodic semigroups founds its generalization with an appropriate notion of aperiodic omega-semigroup. Logic comes in with Chapter 8. The main point is that there is a close connexion between the concepts of automata theory and those of logic, as it was the case with topology. Thus, recognizability is equivalent with monadic second order definability while aperiodicity is equivalent to first order definability. The last two chapters deal with two natural extensions of infinite words. The first one is concerned with two-sided infinite words, for which all notions generalize in a natural way. The second one deals with infinite trees. This case is important because of its role in the applications. The situation is very different with trees instead of words and, in particular, Büchi and Muller automata are no longer equivalent. The main result is Rabin's theorem which states the equivalence between recognizability by tree automata and monadic second order definability