Finkel, Olivier Infinite games specified by 2-tape automata. (English) Zbl 1422.03113 Ann. Pure Appl. Logic 167, No. 12, 1184-1212 (2016). Summary: 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) \(\mathcal{A}\) such that: (a) there is a model of ZFC in which Player 1 has a winning strategy \(\sigma\) in the game \(G(L(\mathcal{A}))\) but \(\sigma\) cannot be recursive and not even in the class \((\operatorname{\Sigma}_2^1 \cup \operatorname{\Pi}_2^1)\); (b) there is a model of ZFC in which the game \(G(L(\mathcal{A}))\) is not determined.2. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) \(\mathcal{A}\) such that \(L(\mathcal{A})\) is an arithmetical \(\operatorname{\Delta}_3^0\)-set and Player 2 has a winning strategy in the game \(G(L(\mathcal{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) \(\mathcal{A}_n\), \(n \geq 1\), such that all games \(G(L(\mathcal{A}_n))\) are determined, but for which it is \(\operatorname{\Pi}_2^1\)-complete hence highly undecidable to determine whether Player 1 has a winning strategy in the game \(G(L(\mathcal{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) \(\mathcal{A}_\sharp\) such that the game \(G(\mathcal{A}_\sharp)\) 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) \((\mathcal{A}_\alpha)_{\alpha < \omega_1^{\operatorname{CK}}}\), indexed by recursive ordinals, such that the games \(G(L(\mathcal{A}_\alpha))\) 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. MSC: 03E60 Determinacy principles 03E35 Consistency and independence results 03D05 Automata and formal grammars in connection with logical questions 68Q45 Formal languages and automata 68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.) 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) 03E15 Descriptive set theory Keywords:automata and formal languages; logic in computer science; Gale-Stewart games; 2-tape Büchi automaton; 1-counter automaton; determinacy; effective analytic determinacy; models of set theory; independence from the axiomatic system ZFC; complexity of winning strategies; wadge games PDFBibTeX XMLCite \textit{O. Finkel}, Ann. Pure Appl. Logic 167, No. 12, 1184--1212 (2016; Zbl 1422.03113) Full Text: DOI arXiv References: [1] Arnold, A.; Duparc, J.; Niwiński, D.; Murlak, F., On the topological complexity of tree languages, (Logic and Automata. Logic and Automata, Texts Log. Games, vol. 2 (2008), Amsterdam Univ. Press: Amsterdam Univ. Press Amsterdam), 9-28 · Zbl 1244.03116 [2] Blass, A., Complexity of winning strategies, Discrete Math., 3, 295-300 (1972) · Zbl 0243.90052 [3] Cachat, T., Higher order pushdown automata, the Caucal hierarchy of graphs and parity games, (Proceedings of the 30th International Colloquium on Automata, Languages and Programming. Proceedings of the 30th International Colloquium on Automata, Languages and Programming, ICALP 2003, Eindhoven, The Netherlands, June 30-July 4, 2003. Proceedings of the 30th International Colloquium on Automata, Languages and Programming. Proceedings of the 30th International Colloquium on Automata, Languages and Programming, ICALP 2003, Eindhoven, The Netherlands, June 30-July 4, 2003, Lecture Notes in Comput. Sci., vol. 2719 (2003), Springer), 556-569 · Zbl 1039.68063 [4] Carayol, A.; Hague, M.; Meyer, A.; Ong, C.-H. L.; Serre, O., Winning regions of higher-order pushdown games, (Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science. Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, Pittsburgh, PA, USA, 24-27 June, 2008 (2008), IEEE Computer Society), 193-204 [5] Castro, J.; Cucker, F., Nondeterministic \(ω\)-computations and the analytical hierarchy, J. Math. Logik Grund. Math., 35, 333-342 (1989) · Zbl 0661.03030 [6] Cohen, R.; Gold, A., \(ω\)-computations on Turing machines, Theoret. Comput. Sci., 6, 1-23 (1978) · Zbl 0368.68057 [7] Finkel, O., Borel ranks and Wadge degrees of omega context free languages, Math. Structures Comput. Sci., 16, 5, 813-840 (2006) · Zbl 1121.03047 [8] Finkel, O., On the accepting power of two-tape Büchi automata, (Proceedings of the 23rd International Symposium on Theoretical Aspects of Computer Science. Proceedings of the 23rd International Symposium on Theoretical Aspects of Computer Science, STACS 2006. Proceedings of the 23rd International Symposium on Theoretical Aspects of Computer Science. Proceedings of the 23rd International Symposium on Theoretical Aspects of Computer Science, STACS 2006, Lecture Notes in Comput. Sci., vol. 3884 (2006), Springer), 301-312 · Zbl 1137.03023 [9] Finkel, O., Wadge degrees of infinitary rational relations, Special Issue on Intensional Programming and Semantics in Honour of Bill Wadge on the Occasion of His 60th Cycle. Special Issue on Intensional Programming and Semantics in Honour of Bill Wadge on the Occasion of His 60th Cycle, Math. Comput. Sci., 2, 1, 85-102 (2008) · Zbl 1157.03017 [10] Finkel, O., Highly undecidable problems for infinite computations, Theor. Inform. Appl., 43, 2, 339-364 (2009) · Zbl 1171.03024 [11] Finkel, O., The complexity of infinite computations in models of set theory, Log. Methods Comput. Sci., 5, 4:4, 1-19 (2009) · Zbl 1191.03034 [12] Finkel, O., The determinacy of context-free games, (Dürr, C.; Wilke, T., 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012), LIPIcs. Leibniz Int. Proc. Inform., vol. 14 (2012)), 555-566 · Zbl 1254.03077 [13] Finkel, O., The determinacy of context-free games, J. Symbolic Logic, 78, 4, 1115-1134 (2013) · Zbl 1349.03038 [14] Gale, D.; Stewart, F. M., Infinite games with perfect information, (Contributions to the Theory of Games, vol. 2. Contributions to the Theory of Games, vol. 2, Ann. of Math. Stud., vol. 28 (1953), Princeton University Press: Princeton University Press Princeton, NJ), 245-266 · Zbl 0050.14305 [15] Harrington, L., Analytic determinacy and \(0^\sharp \), J. Symbolic Logic, 43, 4, 685-693 (1978) · Zbl 0398.03039 [16] Hopcroft, J. E.; Motwani, R.; Ullman, J. D., Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Ser. Comput. Sci. (2001), Addison-Wesley Publishing Co.: Addison-Wesley Publishing Co. Reading, MA · Zbl 0980.68066 [17] Jech, T., Set Theory (2002), Springer [18] Kechris, A. S., Classical Descriptive Set Theory (1995), Springer-Verlag: Springer-Verlag New York · Zbl 0819.04002 [19] Kunen, K., Set Theory - An Introduction to Independence Proofs, Stud. Logic Found. Math., vol. 102 (1980), North-Holland Publishing Co.: North-Holland Publishing Co. Amsterdam · Zbl 0443.03021 [20] Lescow, H.; Thomas, W., Logical specifications of infinite computations, (de Bakker, J. W.; de Roever, W. P.; Rozenberg, G., A Decade of Concurrency. A Decade of Concurrency, Lecture Notes in Comput. Sci., vol. 803 (1994), Springer), 583-621 [21] Louveau, A.; Saint-Raymond, J., The strength of Borel Wadge determinacy, (Cabal Seminar 81-85. Cabal Seminar 81-85, Lecture Notes in Math., vol. 1333 (1988), Springer), 1-30 · Zbl 0651.03036 [22] Martin, D. A., Measurable cardinals and analytic games, Fund. Math., 66, 287-291 (1969/1970) · Zbl 0216.01401 [23] McAloon, K., Les théorèmes de Martin et de Harrington. Applications et remarques, (Set Theory: GMS Seminar. Set Theory: GMS Seminar, Paris, 1976-1977 and 1977-1978. Set Theory: GMS Seminar. Set Theory: GMS Seminar, Paris, 1976-1977 and 1977-1978, Publ. Math. Univ. Paris VII, vol. 5 (1979), Université Paris VII: Université Paris VII Paris), 203-222 [24] Nemoto, T.; Ould MedSalem, M.; Tanaka, K., Infinite games in the Cantor space and subsystems of second order arithmetic, MLQ Math. Log. Q., 53, 3, 226-236 (2007) · Zbl 1122.03058 [25] Odifreddi, P., Classical Recursion Theory, vol. I, Stud. Logic Found. Math., vol. 125 (1989), North-Holland Publishing Co.: North-Holland Publishing Co. Amsterdam · Zbl 0931.03057 [26] Odifreddi, P., Classical Recursion Theory, vol. II, Stud. Logic Found. Math., vol. 143 (1999), North-Holland Publishing Co.: North-Holland Publishing Co. Amsterdam · Zbl 0931.03057 [27] Perrin, D.; Pin, J.-E., Infinite Words, Automata, Semigroups, Logic and Games, Pure Appl. Math., vol. 141 (2004), Elsevier · Zbl 1094.68052 [28] Rogers, H., Theory of Recursive Functions and Effective Computability (1967), McGraw-Hill: McGraw-Hill New York · Zbl 0183.01401 [29] Sami, R. L., Analytic determinacy and \(0^\sharp \). A forcing-free proof of Harrington’s theorem, Fund. Math., 160, 2, 153-159 (1999) · Zbl 0933.03069 [30] Selivanov, V., Wadge degrees of \(ω\)-languages of deterministic Turing machines, RAIRO Theor. Inform. Appl., 37, 1, 67-83 (2003) · Zbl 1048.03031 [31] Selivanov, V., Wadge reducibility and infinite computations, Math. Comput. Sci., 2, 1, 5-36 (2008) · Zbl 1157.03018 [32] Staiger, L., \(ω\)-languages, (Handbook of Formal Languages, vol. 3 (1997), Springer: Springer Berlin), 339-387 [33] Staiger, L., On the power of reading the whole infinite input tape, (Finite Versus Infinite: Contributions to an Eternal Dilemma. Finite Versus Infinite: Contributions to an Eternal Dilemma, Discrete Math. Theor. Comput. Sci. (2000), Springer-Verlag: Springer-Verlag London), 335-348 [34] Stern, J., Analytic equivalence relations and coanalytic games, (Patras Logic Symposion. Patras Logic Symposion, Patras, 1980. Patras Logic Symposion. Patras Logic Symposion, Patras, 1980, Stud. Logic Found. Math., vol. 109 (1982), North-Holland: North-Holland Amsterdam), 239-260 [35] Thomas, W., On the synthesis of strategies in infinite games, (Proceedings of the International Conference STACS 1995. Proceedings of the International Conference STACS 1995, Lecture Notes in Comput. Sci., vol. 900 (1995), Springer), 1-13 · Zbl 1379.68233 [36] Thomas, W., Church’s problem and a tour through automata theory, (Avron, A.; Dershowitz, N.; Rabinovich, A., Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Lecture Notes in Comput. Sci., vol. 4800 (2008), Springer), 635-655 · Zbl 1133.68367 [37] Wadge, W., Reducibility and determinateness in the Baire space (1983), University of California: University of California Berkeley, Ph.D. thesis [38] Walukiewicz, I., Pushdown processes: games and model checking, Inform. and Comput., 157, 234-263 (2000) · Zbl 1003.68072 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.