Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an unbounded or infinite alphabet. They provide a simple formalism to specify the behaviour of reactive systems operating over data
Thus, we study one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show they are determined, and deciding the existence of a winning strategy is in ExpTime, both for $\mathbb{Q}$ and $\mathbb{N}$. This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to
While generalising our results about register-bounded and unbounded synthesis over $(\mathbb{N},=)$ (presented here) to the case of $(\mathbb{Q},<)$ is relatively straightforward, the case of $(\mathbb{N},<)$ is significantly more difficult, as behaviours of register automata over the latter domain cannot be abstracted in an $\omega$‑regular way. In this paper, we however show that they can be regularly approximated. This contribution is detailed in Chapter 7 of my manuscript (more precisely Section 7.3.4), which also features a simpler proof of the key lemma (Lemma 16 in the paper, 7.25 in the manuscript).
Ayrat presented this work at STACS 2021. He also gave a more in-depth talk about it at the IRIF “Automates” seminar. The link is not public, but you might consider contacting the organisers of the seminar to ask for it.