Church synthesis on register automata over linearly ordered data domains

In a Church synthesis game, two players, Adam and Eve, alternately pick some element in a finite alphabet, for an infinite number of rounds. The game is won by Eve if the ω -word formed by this infinite interaction belongs to a given language S , called the specification. It is well-known that for ω -regular specifications, it is decidable whether Eve has a strategy to enforce the specification no matter what Adam does. We study the extension of Church synthesis games to the linearly ordered data domains (ℚ,≤ ) and (ℕ,≤ ) . In this setting, the infinite interaction between Adam and Eve results in an ω - data word, i.e., an infinite sequence of elements in the domain. We study this problem when specifications are given as register automata. Those automata consist in finite automata equipped with a finite set of registers in which they can store data values, that they can then compare with incoming data values with respect to the linear order. Church games over (ℕ,≤ ) are however undecidable, even for deterministic register automata. Thus, we introduce one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show that they are determined, and that deciding the existence of a winning strategy is in ExpTime , both for ℚ and ℕ . This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to ω -regular games. We present an application of one-sided Church games to a transducer synthesis problem. In this application, a transducer models a reactive system (Eve) which outputs data stored in its registers, depending on its interaction with an environment (Adam) which inputs data to the system.