Approximate Problems for Finite Transducers
Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, Saina Sunny
TL;DR
This work investigates approximate counterparts of classical problems for finite transducers that define rational relations, introducing distance-based notions to compare functions and relations. It establishes decidability of approximate determinisation for rational functions with respect to Levenshtein-family distances and for Hamming distance by leveraging ATP, STP, and (for Hamming) HTP, and it provides constructive methods to obtain sequential approximants. It also proves decidability of the approximate functionality problem while showing the approximate uniformisation problem to be undecidable, leveraging diameter/Conjugacy properties and PCP-based reductions. The results combine twinning-property techniques with component-wise decompositions to translate non-deterministic transducers into finite unions of sequential components, enabling synthesis under bounded distortion. Collectively, these findings deepen understanding of when finite transducers can be effectively approximated by sequential devices, with implications for verification, synthesis, and formal language theory.
Abstract
Finite (word) state transducers extend finite state automata by defining a binary relation over finite words, called rational relation. If the rational relation is the graph of a function, this function is said to be rational. The class of sequential functions is a strict subclass of rational functions, defined as the functions recognised by input-deterministic finite state transducers. The class membership problems between those classes are known to be decidable. We consider approximate versions of these problems and show they are decidable as well. This includes the approximate functionality problem, which asks whether given a rational relation (by a transducer), is it close to a rational function, and the approximate determinisation problem, which asks whether a given rational function is close to a sequential function. We prove decidability results for several classical distances, including Hamming and Levenshtein edit distance. Finally, we investigate the approximate uniformisation problem, which asks, given a rational relation $R$, whether there exists a sequential function that is close to some function uniformising $R$. As for its exact version, we prove that this problem is undecidable.
