Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk)
Determinacy of infinite two-player games is a topic of descriptive set theory that has triggered intensive research in theoretical computer science since 1957 when A. Church formulated his "synthesis problem" (regarding the construction of circuits with infinite behavior from logical specifications). In the first part of the lecture we review the fascinating development of the algorithmic theory of infinite games that was started by Church's problem, that enriched automata theory and related fields, and that led to interesting applications in verification and program synthesis. In the second part we turn to the question how to lift this theory from the case of the Cantor space (where a play is a sequence of bits) to the case of the Baire space (where a play is a sequence of natural numbers). While this step does not involve difficulties in classical descriptive set theory, the algorithmic approach raises non-trivial questions since it requires to consider automata that work over infinite alphabets. We present recent results (joint work with B. BrÃ¼tsch) that provide a solution of Church's synthesis problem in this context, and we point to numerous questions that are still open.
Infinite games
descriptive set theory
automata theory
transducers
automatic synthesis
6:1-6:1
Invited Talk
Wolfgang
Thomas
Wolfgang Thomas
10.4230/LIPIcs.CSL.2017.6
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode