Resynchronized Uniformization and Definability Problems for Rational Relations
Christof Löding, Sarah Winter
TL;DR
This work develops a unified framework for uniformization and definability problems of rational word relations using regular synchronization languages. It extends classical results on automatic and recognizable relations by enabling more expressive synchronization constraints and studying both fixed and input-specified target languages; it provides new decidability and undecidability results, with reductions to distance automata and careful analyses of minsync/maxsync/allsync representations. The paper establishes decidability in several important cases (e.g., uniformization by recognizable relations, automatic relations with finite shiftlag targets under certain conditions, and definability when targets are unambiguous or prefix-recognizable) and demonstrates undecidability in broad settings (notably for general uniformization with subsequential transducers and for automatic sources under arbitrary target synchronization). Overall, it clarifies which combinations of source/target classes yield algorithmic solvability and which remain intractable, contributing a systematic map for future work in synchronization-language-based relational definability. The results have potential implications for origin semantics, reactive synthesis, and decision procedures in logic over word relations.
Abstract
Regular synchronization languages can be used to define rational relations of finite words, and to characterize subclasses of rational relations, like automatic or recognizable relations. We provide a systematic study of the decidability of uniformization and definability problems for subclasses of rational relations defined in terms of such synchronization languages. We rephrase known results in this setting and complete the picture by adding several new decidability and undecidability results.