The Complexity of Transducer Synthesis from Multi-Sequential Specifications (MFCS 2018)


The transducer synthesis problem on finite words asks, given a specification $S \subseteq I \times O$, where $I,O$ are sets of finite words, whether there exists a function $f$ which (1) fulfils the specification, i.e. $(i,f(i))\in S$ for all $i\in I$, and (2) can be defined by some input-deterministic (aka sequential) transducer $\mathcal{T}$. If such an $f$ exists, the procedure should also output $\mathcal{T}$. For specifications given by synchronous transducers (which read and write alternately one symbol), this problem is the finite variant of the classical synthesis problem on $\omega$‑words, solved by Büchi and Landweber in 1969, and is known, in both finite and $\omega$‑word settings, to be ExpTime-complete.

In the asynchronous setting (where a transducer can write a batch of symbols, or none, in a single step), this problem is known to be undecidable. We consider here the class of multi-sequential specifications, defined as finite unions of sequential transducers (over possibility incomparable domains). In both settings, asynchronous and synchronous, we provide optimal decision procedures by showing the problem to be PSpace-complete.

43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, August 27-31, 2018, Liverpool, UK