Uniformization Problems for Synchronizations of Automatic Relations on Words

TL;DR

This paper investigates the problem of uniformizing automatic relations with functions implemented by specific classes of transducers, introducing a new variant with synchronization constraints and proving its decidability for certain classes.

Contribution

It introduces a new variant of the uniformization problem with synchronization constraints and proves its decidability for a specific class of synchronizations.

Findings

Decidability established for the new synchronization-constrained uniformization variant.

Extension of known decidability results to a broader class of transducer behaviors.

Formal framework for analyzing uniformizations with synchronization specifications.

Abstract

A uniformization of a binary relation is a function that is contained in the relation and has the same domain as the relation. The synthesis problem asks for effective uniformization for classes of relations and functions that can be implemented in a specific way. We consider the synthesis problem for automatic relations over finite words (also called regular or synchronized rational relations) by functions implemented by specific classes of sequential transducers. It is known that the problem "Given an automatic relation, does it have a uniformization by a subsequential transducer?" is decidable in the two variants where the uniformization can either be implemented by an arbitrary subsequential transducer or it has to be implemented by a synchronous transducer. We introduce a new variant of this problem in which the allowed input/output behavior of the subsequential transducer is specified by a set of synchronizations and prove decidability for a specific class of synchronizations.