摘要：In reactive synthesis, the goal is to automatically generate animplementation from a specification of the reactive and non-terminatinginput/output behaviours of a system. Specifications are usually modelled aslogical formulae or automata over infinite sequences of signals($\omega$-words), while implementations are represented as transducers. In theclassical setting, the set of signals is assumed to be finite. In this paper,we consider data $\omega$-words instead, i.e., words over an infinite alphabet.In this context, we study specifications and implementations respectively givenas automata and transducers extended with a finite set of registers. Weconsider different instances, depending on whether the specification isnondeterministic, universal or deterministic, and depending on whether thenumber of registers of the implementation is given or not. In the unbounded setting, we show undecidability for both universal andnondeterministic specifications, while decidability is recovered in thedeterministic case. In the bounded setting, undecidability still holds fornondeterministic specifications, but can be recovered by disallowing tests overinput data. The generic technique we use to show the latter result allows us toreprove some known result, namely decidability of bounded synthesis foruniversal specifications.
关键词：Computer Science - Formal Languages and Automata Theory
