In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (
In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.
This work is an extension of Synthesis of Data Word Transducers (CONCUR 2019). It contains full proofs and provides a simplified proof for the unbounded case. The proofs have been further distilled in Chapters 5-7 of my manuscript.
It also includes a discussion on the relation between synthesis and uniformisation problems, in particular on the aspect of the domain of the specification. Such distinction does not matter much in the finite alphabet case, as $\omega$‑regular languages are closed under complement. Thus, any specification can be extended to one with a total domain by allowing any behaviour on the complement of the domain. However, it makes a big difference in the infinite alphabet case, since languages recognised register automata are not closed under complement. This question is explored in more depth in Chapter 8 of my thesis.