Deciding the Topological Complexity of Büchi Languages
Michał Skrzypczak, Igor Walukiewicz · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2016
We study the topological complexity of languages of Büchi automata on infinite binary trees. We show that such a language is either Borel and WMSO-definable, or Sigma_1^1-complete and not WMSO-definable; moreover it can be algorithmically decided which of the two cases holds. The proof relies on a direct reduction to deciding the winner in a finite game with a regular winning condition.