Descriptive set theoretic methods in automata theory

Poniższa rozprawa jest poświęcona badaniom problemów teorii automatów z punktu widze- nia deskryptywnej teorii mnogości. Analizowane struktury to nieskończone słowa i drzewa. Większość zaprezentowanych rezultatów ma formę algorytmu, który operuje na reprezen- tacjach języków regularnych. Szczególny wysiłek jest włożony w opracowanie efektywnych charakteryzacji języków regularnych drzew nieskończonych, definiowalnych w słabej monadycznej logice drugiego rzędu ( wmso ). Jakkolwiek nie jest znana żadna taka charakteryzacja dla ogólnych języków regularnych, rozprawa dostarcza charakteryzacji w pewnych szczególnych przypadkach: dla automatów growych, dla języków drzew cienkich (posiadających tylko przeliczalnie wiele gałęzi) i dla automatów Büchiego. Dodatkowo są udowodnione pewne związki pomiędzy definiowalnością w wmso a zbiorami borelowskimi. Innym problemem studiowanym w ramach rozprawy jest problem indeksu alternującego (zwany też problemem indeksu Rabina-Mostowskiego). Podobnie jak w przypadku wmso problem ten w pełnej ogólności wydaje się być poza zasięgiem aktualnie znanych metod. W ramach rozprawy zaproponowana jest procedura rozstrzygająca problem indeksu dla au- tomatów growych. Stanowią one obecnie najszerszą klasę automatów dla których problem indeksu został rozwiązany. Dodatkowo rozprawa zajmuje się zagadnieniem algebraicznych metod rozpoznawania języków regularnych drzew nieskończonych. W tym celu wprowadzone zostaje pojęcie pro- phetic thin algebra . Wykazane jest, że algebry te rozpoznają dokładnie klasę języków po- dwójnie jednoznacznych — języków L takich, że L oraz dopełnienie L c mogą być rozpozna- wane przez automaty jednoznaczne. Dodatkowo nowa hipoteza dotycząca definiowalności funkcji wyboru jest postawiona. Wyniki rozprawy pokazują, że owa hipoteza jest ściśle związana z klasą prophetic thin algebras . W szczególności hipoteza ta implikuje istnienie efektywnej charakteryzacji klasy języków podwójnie jednoznacznych. Wreszcie rozprawa przedstawia badania niedawno zaproponowanych ilościowych roz- szerzeń klasy języków regularnych. Po pierwsze udowodnione są ograniczenia dolne (od- powiadające ograniczeniom górnym) na złożoność topologiczną języków słów nieskończo- nych definiowalnych w mso+u . Ograniczenia te służą do wykazania, że logika mso+u jest nierozstrzygalna na drzewie nieskończonym (przy pewnych dodatkowych założeniach teoriomnogościowych). Dodatkowo jest wykazane, że klasy języków rozpoznawane przez pewne automaty licznikowe mają własność separacji ze względu na języki regularne słów nieskończonych. Dowód tego twierdzenia korzysta z metod topologicznych w monoidzie słów proskończonych.

This thesis is devoted to studying problems of automata theory from the point of view of descriptive set theory. The analyzed structures are ω -words and infinite trees. Most of the presented results have a form of an effective decision procedure that operates on representations of regular languages. A particular effort is put into providing effective characterisations of regular languages of infinite trees that are definable in weak monadic second-order logic ( wmso ). Although no such characterization is known for all regular languages of infinite trees, the thesis provides characterisations in some special cases: for game automata, for languages of thin trees (i.e. trees with countably many branches), and for Büchi automata. Additionally, certain relations between wmso -definable languages and Borel sets are proved. Another problem studied in the thesis is the alternating index problem (also called Rabin-Mostowski index problem). Again, the problem in its full generality seems to be out of reach of the currently known methods. However, a decision procedure for the class of game automata is proposed in the thesis. These automata form the widest class of automata for which the problem is currently known to be decidable. The thesis also addresses the problem of providing an algebraic framework for regular languages of infinite trees. For this purpose the notion of prophetic thin algebras is intro- duced. It is proved that finite prophetic thin algebras recognize exactly the bi-unambiguous languages — languages L such that both L and the complement L c can be recognised by unambiguous automata. Additionally, a new conjecture about definability of choice func- tions is stated. It is proved that this conjecture is strongly related to the class of prophetic thin algebras. In particular, the conjecture implies an effective characterisation of the class of bi-unambiguous languages. Finally, the thesis studies contemporary quantitative extensions of the class of regular languages. First, lower bounds (that match upper bounds) on the topological complexity of mso+u -definable languages of ω -words are given. These lower bounds can be used to prove that mso+u logic is undecidable on infinite trees in a specific sense. It is also shown that languages of ω -words recognisable by certain counter automata have the separation property with respect to ω -regular languages. The proof relies on topological methods in the profinite monoid. 1