Infinite games specified by 2-tape automata.

We prove that the determinacy of Gale–Stewart games whose winning sets are infinitary rational relations accepted 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. Then we prove that winning strategies, when they exist, can be very complex, i.e. highly non-effective, in these games. We prove the same results for Gale–Stewart games with winning sets accepted by real-time 1-counter Büchi automata, then extending previous results obtained about these games. 1. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A such that: (a) there is a model of ZFC in which Player 1 has a winning strategy σ in the game G ( L ( A ) ) but σ cannot be recursive and not even in the class ( Σ 2 1 ∪ Π 2 1 ) ; (b) there is a model of ZFC in which the game G ( L ( A ) ) is not determined. 2. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A such that L ( A ) is an arithmetical Δ 3 0 -set and Player 2 has a winning strategy in the game G ( L ( A ) ) but has no hyperarithmetical winning strategies in this game. 3. There exists a recursive sequence of 2-tape Büchi automata (respectively, of real-time 1-counter Büchi automata) A n , n ≥ 1 , such that all games G ( L ( A n ) ) are determined, but for which it is Π 2 1 -complete hence highly undecidable to determine whether Player 1 has a winning strategy in the game G ( L ( A n ) ) . Then we consider the strengths of determinacy for these games, and we prove the following results. 1. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A ♯ such that the game G ( A ♯ ) is determined iff the effective analytic determinacy holds. 2. There is a transfinite sequence of 2-tape Büchi automata (respectively, of real-time 1-counter Büchi automata) ( A α ) α < ω 1 CK , indexed by recursive ordinals, such that the games G ( L ( A α ) ) have strictly increasing strengths of determinacy. We also show that the determinacy of Wadge games between two players in charge of infinitary rational relations accepted by 2-tape Büchi automata is equivalent to the (effective) analytic Wadge determinacy and thus also equivalent to the (effective) analytic determinacy. [ABSTRACT FROM AUTHOR]