The Büchi-Landweber theorem establishes decidability and effective synthesis of winning strategies in regular infinite games played on finite arenas. In this work, we generalise this theorem to games whose arenas are infinite words. The setting is as follows. There is a fixed infinite word p (a parameter). For each position, Player I and then Player II produce one additional letter, yielding a word with three tracks: the parameter track and one track for each player. Finally, to find a winner, we check whether the word belongs to some regular language W.

We obtain results on three levels. First, deciding the winner: given the regular winning condition W, one can construct a regular language of those parameter words p over which Player II can win. Second, synthesis of finite-memory strategies: based on W, one can construct a finite-memory transducer equipped with regular lookahead on the parameter word p, which generates a winning strategy of Player II. Third, elimination of lookahead in the special case of separated winning conditions: if the winning condition is a Boolean combination of languages depending only on the parameter track and Player I's track, and languages depending only on Player II's track, then a winning strategy of Player II can be generated by a finite-memory transducer without any lookahead (while in general some lookahead is necessary).

The winner determination result is folklore and follows from work of Kaiser. The next two results are novel. The key step for the second result is uniformisation of MSO formulae, which allows us to select a particular winning strategy, and then to synthesise it. For the third result, we work with Wilke algebras to obtain a constructive variant of Ramsey's theorem, building on a technical idea due to Thomas.

This presentation is based on the paper Generalised Quantifiers Based on Rabin-Mostowski Index published on STACS 2026; co-authors: Denis Kuperberg, Damian Niwiński, Michał Skrzypczak.