On Synthesis of Resynchronizers for Transducers

TL;DR

This paper investigates the formal comparison of transducers under origin semantics using resynchronizers, establishing decidability results for synthesis problems in various classes of transducers, with some cases remaining open.

Contribution

It introduces a formal framework for comparing transducers via resynchronizers and proves decidability of synthesis problems for specific classes of transducers, extending understanding of origin semantics.

Findings

Synthesis of rational resynchronizers is decidable for functional and finite-valued one-way transducers.

Synthesis of rational resynchronizers is undecidable for relational one-way transducers.

Synthesis of regular resynchronizers is decidable for unambiguous two-way transducers.

Abstract

We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T1, T2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T1 is contained in R(T2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open.