Descriptive set theoretic methods in automata theory. Decidability and topological complexity (Q737116)

This book is based on the author's PhD thesis, which was awarded the E.W. Beth Prize 2015 by the Association for Logic, Language and Information (FoLLI) for its outstanding contribution to the fields of logic, language, and information. The results presented in the book are based on the published papers [\textit{S. Hummel} and the author, Fundam. Inform. 119, No. 1, 87--111 (2012; Zbl 1260.03075); \textit{M. Bojańczyk} et al., LIPICS -- Leibniz Int. Proc. Inform. 20, 562--573 (2013; Zbl 1354.68146); \textit{M. Bilkowski} and the author, LIPICS -- Leibniz Int. Proc. Inform. 23, 81--100 (2013; Zbl 1356.68128); the author, Log. Methods Comput. Sci. 10, No. 1, Paper No. 8, 1--20 (2014; Zbl 1325.68134); \textit{M. Bojańczyk} et al., Lect. Notes Comput. Sci. 8573, 50--61 (2014; Zbl 1407.03007)] and on the technical report [\textit{H. Michalewski} and the author, ``Unambiguous Büchi is weak'', Preprint, \url{arXiv:1401.4025}]. This book considers finite automata on infinite words (\(\omega\)-words, \(\omega\)-automata) and also on infinite trees (tree automata). By the seminal results of Büchi and Rabin, there is a correspondence between an \(\omega\)-automaton and monadic second-order (MSO) logic formulas on \(\langle \omega,\leq\rangle\) and between (non-deterministic) tree automata and MSO formulas on \(\langle \{0,1\}^*,\preceq,\leq_{\text{lex}}\rangle\) (i.e., finite words on \(\{0,1\}\) with prefix and lexicographic ordering). This yields the decidability of the MSO theories of these structures and was the starting point of the development of the logic-based approach to automata theory. While non-deterministic and deterministic automata are equivalent in the expressive power for \(\omega\)-words, this is not the case for infinite trees. The study of tree automata hence calls for more advanced methods, as those presented in this book. For an automaton \(\mathcal{A}\), one usually considers its \textit{language} \(L(\mathcal{A})\), which is the set of words or trees that have an accepting run on \(\mathcal{A}\). A language (as set of words or trees) is then said to be \textit{regular} if it is accepted by some (non-deterministic) automaton. Accepting conditions are nowadays usually specified using parity automata, where each state is associated with a natural number, its \textit{priority}, and a run is \textit{accepting} if the smallest priority that occurs infinitely often during the run (or on infinite branches in the case of tree automata) is even. The book also considers alternating automata, where transitions have a more complex structure. In this setting, the \textit{index} of an automaton \((i,j)\) is the pair formed by the minimal and maximal priorities of states of the automaton. An alternating automaton is furthermore said to be \(\mathrm{Comp}(i,j)\) if each strongly connected component of the automaton has priorities between \(i\) and \(j\) or between \(i+1\) and \(j+1\). An automaton is called Büchi when its index is \((0,1)\). While alternating and non-deterministic automata have equal expressive power, indexes are usually not preserved. The book's first chapter presents basic definitions and results, which are used in the following chapters. This makes the book pretty much self-contained and accessible even to a non-specialist having a basic familiarity with automata theory. Chapter 2, the introduction, presents current research questions on \(\omega\)- and tree automata and shows how the results of this book contribute to the advancement of knowledge on these topics. Chapter 3 considers weak monadic second-order logic (WMSO), where set quantification is interpreted over finite sets. While definability in MSO and WMSO is equivalent for \(\omega\)-languages, WMSO logic is strictly weaker for trees. The characterization of those MSO definable languages, which are WMSO-definable, is an important open question in automata theory. This chapter considers a generalization of deterministic automata, namely \textit{unambiguous automata}, where there is at most one accepting run for any input. Chapter 3 presents the result that for an unambiguous automaton \(\mathcal{A}\) of index \((0,j)\), its language \(L(\mathcal{A})\) can be recognized by an alternating \(\mathrm{Comp}(0,j-1)\)-automaton of size polynomial in that of \(\mathcal{A}\). In particular, if \(\mathcal{A}\) is Büchi and unambiguous, then \(L(\mathcal{A})\) is WMSO-definable. The proof uses an automata theoretic adaptation of methods from descriptive set theory. It is shown in Chapter 4 that it is decidable whether the language of infinite trees recognized by a given non-deterministic Büchi tree automaton is WMSO-definable. This result was already shown by [\textit{T. Colcombet} et al., LIPICS -- Leibniz Int. Proc. Inform. 23, 215--230 (2013; Zbl 1356.68129)], but in this chapter the author presents a completely different proof relying on a complexity measure of trees with respect to a given Büchi automaton, which yields an ordinal rank on automata. The author then shows that this ordinal is strongly related to the descriptive complexity of the automaton's language. Chapter 5 considers the game automata of \textit{J. Duparc} et al. [LIPICS -- Leibniz Int. Proc. Inform. 13, 363--374 (2011; Zbl 1246.68142)], which form a class extending that of deterministic automata that is closed under complementation and composition, while preserving some natural equivalence relations on recognized languages. The chapter shows that determining both the non-deterministic and the alternating index is decidable for game automata. The proofs uses an analysis of runs and of automata structures. The author then considers the set of \(\omega\)-words and of trees as topological spaces (under the product topology). In this setting, he considers the Borel (\(\boldsymbol{\Sigma}_\alpha^0\), \(\boldsymbol{\Pi_\alpha^0}\)) and the analytic (\(\boldsymbol{\Sigma}_\alpha^1\), \(\boldsymbol{\Pi_i^1}\)) hierarchies. He furthermore uses the notions of reduction and completeness for elements of the Borel and analytic hierarchies. Chapter 6 considers \textit{thin trees}, which are trees containing only countably many infinite branches. The author shows that a regular language containing only thin trees is either \(\boldsymbol{\Pi_1^1}\)-complete among all infinite trees or WMSO-definable among all infinite trees (and hence Borel). Moreover, he also shows that it is decidable which case holds. The proof uses a decomposition of thin trees and a concept of \textit{thin algebra}. Regular languages for finite and \(\omega\)-words can be characterized in algebraic terms using monoids and \(\omega\)-semigroups. In a similar way, Chapter 7 introduces in the context of infinite trees \textit{prophetic thin algebra}. The author shows that a language of infinite trees \(L\) is recognized by a homomorphism into a finite prophetic thin algebra if and only if \(L\) is bi-unambiguous (both \(L\) and its complement \(L^c\) can be recognized by unambiguous automata). In the next chapter, the author considers Conjecture 8.1, i.e., that there is no MSO-definable choice function on thin trees, i.e. there is no formula \(\psi(x,X)\) such that for every thin tree \(t\) and every non-empty \(X\) a subset of the domain of \(t\), the formula \(\psi(x,X)\) is satisfied for a unique \(x\in X\). The author then uses a tree labeling induced by a thin algebra homomorphism, called a \textit{marking} and a notion of subset of a thin tree that provides a decomposition in separate branches, called a \textit{skeleton}, to show the following result: Conjecture 8.1 is equivalent to the fact that every finite thin algebra admits some consistent marking on every infinite tree. He furthermore shows that the relation \(\varphi(\sigma,t)\) stating that \(t\) is a thin tree and \(\sigma\) is a skeleton of \(t\) does not admit any MSO-definable uniformization of \(\sigma\). Finally, he proves that the language of all thin trees is ambiguous (it is not recognized by any unambiguous automaton). Chapter 9 considers MSO+U, an expansion of MSO with the unbounded quantifier \(UX\), whose intuitive meaning is that there are arbitrary large finite \(X\). The author then shows that there exists an alphabet \(A\) such that for every \(i>0\) there exists an MSO+U formula \(\varphi_i\) such that the language \(L(\varphi_i)\subseteq A^\omega\) of \(\omega\)-words satisfying \(\varphi_i\) is \(\boldsymbol{\Sigma}_i^1\)-complete. The proof uses encoding of trees into \(\omega\)-words and topological methods. Chapter10 presents the result of [Zbl 1407.03007, loc. cit.] that, assuming \(V=L\) (the constructibility axiom of set theory), it is undecidable if a given sentence of MSO+U is true in the complete binary tree \(\langle \{L,R\}^*;\prec,\leq_{\text{lex}}\rangle\). The proof uses a multi-sorted version of MSO and topological methods. Chapter 11 considers \(\omega\)B- and \(\omega\)S-regular languages introduced by [\textit{M. Bojańczyk}, LIPICS -- Leibniz Int. Proc. Inform. 5, 11--16 (2010; Zbl 1230.68124)], which are languages of \(\omega\)-words that can be recognized by certain models of counter automata with asymptotic acceptance conditions. The author then shows that if \(L_1\), \(L_2\) are disjoint languages of \(\omega\)-words both recognized by \(\omega\)B- (respectively \(\omega\)S-)-automata then there exists an \(\omega\)-regular language \(L_{\text{sep}}\) such that \(L_1\subseteq L_{\text{sep}}\) and \(L_2\subseteq L_{\text{sep}}^c\). Additionally, the construction of \(L_{\text{sep}}\) is effective. The proof uses automata theoretic constructions and topological considerations. Finally, Chapter 12 is a short conclusion. The author applies, with considerable success, a breadth of methods covering descriptive set theory, automata theory, logic and even some classical set theory, to questions on \(\omega\)- and tree automata. While following the author's results requires quite some mathematical knowledge and sophistication, he has managed to present basic material and his own results in such a way as to make these developments accessible to the reader. The book is hence a welcome addition to the author's published papers and should be useful for those who wish to keep in touch with recent developments in automata theory. As to the book's presentation, an index would definitely have been welcome. There are many definitions and concepts, and the notions considered vary from chapter to chapter. An index would hence have been convenient in order to trace back definitions. This is the case, even if Chapter 1 is fairly short, and the definitions introduced there can be readily located. Indeed, many other concepts are introduced elsewhere, leaving the burden on the reader to find out exactly where the definition originates.