Strategies in infinite games : structured reactive programs and transducers over infinite alphabets
- Strategien in unendlichen Spielen: Strukturierte reaktive Programme und Transducer über unendlichen Alphabeten
Brütsch, Benedikt; Thomas, Wolfgang (Thesis advisor); Markey, Nicolas (Thesis advisor); Grohe, Martin (Thesis advisor)
Aachen (2018, 2020)
Dissertation / PhD Thesis
Dissertation, RWTH Aachen University, 2018
The subject of this thesis is the construction of winning strategies in games of the following kind: Two players alternately choose symbols from some fixed alphabet. They play forever, thus composing an infinite sequence of symbols. The winning condition is a set L of such sequences - the second player wins if the resulting sequence is in the set L, otherwise the first player wins. Such games can be used to model the interaction between a so-called reactive system and its environment: The system continually reads input symbols provided by the environment and produces output symbols in response. A winning condition can be regarded as a specification for the system, and a winning strategy for the system constitutes an implementation of that specification. Church's Synthesis Problem is to determine which player has a winning strategy and to present such a strategy in the form of a finite automaton, given an ω-regular winning condition L ⊆ Σ^ω over a finite alphabet Σ. We consider two variants of this problem. The first variant is a refinement of the task, demanding a strategy in the form of a structured reactive program. It was introduced and solved in 2011 by Madhusudan. His solution involves building an alternating two-way co-Büchi tree automaton recognizing the programs that are winning strategies. We present a direct construction of a deterministic bottom-up tree automaton recognizing these programs and give a lower bound for the size of any such automaton. In both approaches, the number of (Boolean) variables available to the programs is crucial, as the time required by the synthesis algorithm is doubly exponential in that number. We show that for certain winning conditions defined in linear temporal logic (LTL), the required number of variables is exponential in the formula size, matching the known upper bound. The second variant of the synthesis problem is a generalization where the players choose symbols from an infinite alphabet instead of a finite one. More precisely, the alphabet is of the form Σ*, for a finite set Σ, so each symbol is a finite word. To represent winning conditions, we define automata over such infinite alphabets, namely ℕ-memory automata. We study closure properties and decidability questions for these automata, both on finite words and on ω-words. Analogously, we introduce ℕ-memory transducers to represent strategies. We show that the synthesis problem is solvable in this setting: Given a winning condition L ⊆ (Σ*)^ω defined by a deterministic ℕ-memory parity automaton, we can determine which player has a winning strategy and construct such a strategy in the form of a deterministic ℕ-memory transducer.