Synthesis of Data Word Transducers (LMCS Special Issue dedicated to CONCUR 2019)

Abstract

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 ($\omega$‑words), while implementations are represented as transducers. In the classical 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 given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given or not.

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.

Publication
Logical Methods in Computer Science

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.

Related