The theory of automata reading infinite words, which is closely related to infinite games, is a rich theory which is used for the specification and verification of non-terminating systems.
We prove that the Wadge hierarchy of omega-languages accepted by 1-counter Büchi automata (or by 2-tape Büchi automata) is equal to the Wadge hierarchy of omega-languages accepted by Büchi Turing machines, which forms the class of effective analytic sets. Moreover the topological complexity of an omega-language accepted by a 1-counter Büchi automaton, or of an infinitary rational relation accepted by a 2-tape Büchi automaton, is not determined by the axiomatic system ZFC. In particular, there is a 1-counter Büchi automaton A (respectively, a 2-tape Büchi automaton B) and two models V1 and V2 of ZFC such that the omega-language L(A) (respectively, the infinitary rational relation L(B)) is Borel in V1 but not in V2. We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Büchi automata (or by 2-tape Büchi automata) is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automaton (respectively, a 2-tape Büchi automaton) A such that: (1) There exists a model of ZFC in which Player 1 has a winning strategy in the Gale-Stewart game G(L(A)); but the winning strategies cannot be recursive and not even hyperarithmetical. (2) There exists a model of ZFC in which the Gale-Stewart game is not determined. We also prove that the determinacy of Wadge games between two players in charge of omega-languages accepted by real-time 1-counter Büchi automata (or by 2-tape Büchi automata) is equivalent to the effective analytic determinacy, and thus is not provable in ZFC.