Solving Infinite Games in the Baire Space

• Autorzy: Brütsch Benedikt , Thomas Wolfgang

Identyfikatory

DOI

10.3233/FI-222119

• Języki publikacji: EN

Abstrakty

EN

Infinite games (in the form of Gale-Stewart games) are studied where a play is a se- quence of natural numbers chosen by two players in alternation, the winning condition being a subset of the Baire space ω^ω . We consider such games defined by a natural kind of parity au- tomata over the alphabet N, called N-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. We show that the classical Büchi-Landweber Theorem (for finite-state games in the Cantor space 2^ω) holds again for the present games: A game defined by a deterministic parity N-MSO-automaton is deter- mined, the winner can be computed, and an N-MSO-transducer realizing a winning strategy for the winner can be constructed.

Słowa kluczowe

EN

computer science; game theory; logic in computer science

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 186, nr 1-4
• Strony: 63--88
• Opis fizyczny: Bibliogr. 33 poz., rys.

Twórcy

autor

Brütsch Benedikt

• Chair of Computer Science 7 RWTH Aachen University, Germany

autor

Thomas Wolfgang

• Chair of Computer Science 7 RWTH Aachen University, Germany

Bibliografia

• 1] Büchi JR, Landweber LH. Solving Sequential Conditions by Finite-State Strategies. Transactions of the American Mathematical Society, 1969. 138:295-311. doi:10.2307/1994916.
• [2] Trakhtenbrot BA, Barzdin YM. Finite Automata - Behavior and Synthesis, volume 1 of Fundamental Studies in Computer Science. North-Holland Pub. Co., Amsterdam, 1973. ISBN 0444104186.
• [3] Grädel E, Thomas W, Wilke T (eds.). Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-36387-4.
• [4] Thomas W. Languages, Automata, and Logic. In: Rozenberg G, Salomaa A (eds.), Handbook of Formal Languages, pp. 389-455. Springer, 1997. doi:10.1007/978-3-642-59126-6_7.
• [5] Brütsch B. Strategies in Infinite Games: Structured Reactive Programs and Transducers over Infinite Alphabets. Ph.D. thesis, RWTH Aachen University, Germany, 2018. doi:10.18154/RWTH-2020-03492.
• [6] Brütsch B, Thomas W. Playing Games in the Baire Space. In: Proceedings of the Cassting Workshop on Games for the Synthesis of Complex Systems (CASSTING 2016), volume 220 of EPTCS. 2016 pp. 13-25. doi:10.4204/EPTCS.220.2.
• [7] Spelten A, Thomas W, Winter S. Trees over Infinite Structures and Path Logics with Synchronization. In: Proceedings of the 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011), volume 73 of EPTCS. 2011 pp. 20-34. doi:10.4204/EPTCS.73.5.
• [8] Czyba C, Spinrath C, Thomas W. Finite Automata Over Infinite Alphabets: Two Models with Transitions for Local Change. In: Proceedings of the 19th International Conference on Developments in Language Theory (DLT 2015), volume 9168 of Lecture Notes in Computer Science. Springer, 2015 pp. 203-214. doi:10.1007/978-3-319-21500-6_16.
• [9] Brütsch B, Landwehr P, Thomas W. N-Memory Automata over the Alphabet N. In: Proceedings of the 11th International Conference on Language and Automata Theory and Applications (LATA 2017), volume 10168 of Lecture Notes in Computer Science. Springer, 2017 pp. 91-102. doi:10.1007/978-3-319-53733-7_6.
• [10] Kaminski M, Francez N. Finite-Memory Automata. Theoretical Computer Science, 1994. 134(2):329-363. doi:10.1016/0304-3975(94)90242-9.
• [11] Bojańczyk M, David C, Muscholl A, Schwentick T, Segoufin L. Two-Variable Logic on Data Words. ACM Transactions on Computational Logic, 2011. 12(4):27. doi:10.1145/1970398.1970403.
• [12] Tan T. An Automata Model for Trees with Ordered Data Values. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012). IEEE Computer Society, 2012 pp. 586-595. doi:10.1109/LICS.2012.69.
• [13] Bojańczyk M, Klin B, Lasota S. Automata Theory in Nominal Sets. Logical Methods in Computer Science, 2014. 10(3). doi:10.2168/LMCS-10(3:4)2014.
• [14] Bojańczyk M, Stefański R. Single-Use Automata and Transducers for Infinite Alphabets. In: Czumaj A, Dawar A, Merelli E (eds.), 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020 pp. 113:1-113:14. doi:10.4230/LIPIcs.ICALP.2020.113.
• [15] Carayol A, Löding C, Niwinski D, Walukiewicz I. Choice Functions and Well-Orderings over the Infinite Binary Tree. Open Mathematics, 2010. 8(4). doi:10.2478/s11533-010-0046-z.
• [16] Rabin MO. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 1969. 141:1-35. doi:10.1090/S0002-9947-1969-0246760-1.
• [17] Gale D, Stewart F. Infinite Games with Perfect Information. In: Contributions to the Theory of Games, Annals of Mathematics Studies, pp. 245-266. Princeton University Press, 1953. doi:10.1515/9781400881970-014.
• [18] Martin DA. Borel Determinacy. Annals of Mathematics, 1975. 102(2):363-371. doi:10.2307/1971035.
• [19] Church A. Logic, Arithmetic, and Automata. In: Proceedings of the International Congress of Mathematicians 1962, pp. 23-35. Institut Mittag-Leffler, Djursholm, 1963.
• [20] McNaughton R. Finite-State Infinite Games. Technical Report MAC-M-125, MIT, 1965.
• [21] Kupferman O, Piterman N, Vardi MY. An Automata-Theoretic Approach to Infinite-State Systems. In: Manna Z, Peled DA (eds.), Time for Verification, volume 6200 of Lecture Notes in Computer Science, pp. 202-259. Springer, 2010. doi:10.1007/978-3-642-13754-9_11.
• [22] Piterman N, Vardi MY. Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems. In: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003). 2003 pp. 381-390. doi:10.1109/LICS.2003.1210078.
• [23] Cachat T. Uniform Solution of Parity Games on Prefix-Recognizable Graphs. Electronic Notes in Theoretical Computer Science, 2003. 68(6):71-84. doi:10.1016/S1571-0661(04)80534-6.
• [24] Caucal D. On the Transition Graphs of Turing Machines. Theoretical Computer Science, 2003. 296(2):195-223. doi:10.1016/S0304-3975(02)00655-2.
• [25] Blumensath A, Colcombet T, Löding C. Logical Theories and Compatible Operations. In: Flum J, Grädel E, Wilke T (eds.), Logic and Automata: History and Perspectives, volume 2 of Texts in Logic and Games Amsterdam University Press, 2008 pp. 73-106.
• [26] Emerson EA, Jutla CS. Tree Automata, Mu-Calculus and Determinacy. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS 1991). IEEE Computer Society, 1991 pp. 368-377. doi:10.1109/SFCS.1991.185392.
• [27] Walukiewicz I. Monadic Second-Order Logic on Tree-Like Structures. Theoretical Computer Science, 2002. 275(1-2):311-346. doi:10.1016/S0304-3975(01)00185-2.
• [28] Carayol A, Hague M. Regular Strategies in Pushdown Reachability Games. In: Proceedings of the 8th International Workshop on Reachability Problems (RP 2014), volume 8762 of Lecture Notes in Computer Science. Springer, 2014 pp. 58-71. doi:10.1007/978-3-319-11439-2_5.
• [29] Landweber LH. Decision Problems for ω-Automata. Mathematical Systems Theory, 1969. 3(4):376-384. doi:10.1007/BF01691063.
• [30] Cachat T, Duparc J, Thomas W. Solving Pushdown Games with a Σ3 Winning Condition. In: Proceedings of the 16th International Workshop/11th Annual Conference of the EACSL on Computer Science Logic (CSL 2002), volume 2471 of Lecture Notes in Computer Science. Springer, 2002 pp. 322-336. doi: 10.1007/3-540-45793-3_22.
• [31] Serre O. Games with Winning Conditions of High Borel Complexity. Theoretical Computer Science, 2006. 350(2-3):345-372. doi:10.1016/j.tcs.2005.10.024.
• [32] Finkel O. Borel Hierarchy and Omega Context Free Languages. Theoretical Computer Science, 2003. 290(3):1385-1405. doi:10.1016/S0304-3975(02)00042-7.
• [33] Finkel O. The Determinacy of Context-Free Games. The Journal of Symbolic Logic, 2013. 78(4):1115-1134. doi:10.2178/jsl.7804050.