Table of Contents
Fetching ...

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.

Approximate Problems for Finite Transducers

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 , whether there exists a sequential function that is close to some function uniformising . As for its exact version, we prove that this problem is undecidable.

Paper Structure

This paper contains 10 sections, 23 theorems, 5 equations, 1 figure, 1 table.

Key Result

Proposition 2

Let $x,y,x',y',u,v$ be words and $c,C \in \mathbb{N}$. For any metric $d$ in table:editdistance, if $d(xu^ky,x'v^{ck}y') \leq C$ for all $k \geq 0$, then $|u| = |v^{c}|$ and the primitive roots of $u$ and $v$ are conjugate.

Figures (1)

  • Figure 1: An unambiguous non-deterministic transducer $\mathcal{T}$, along with two sequential approximations $\mathcal{D}_1$ and $\mathcal{D}_2$ with respect to the Levenshtein distance, respectively Hamming distance.

Theorems & Definitions (32)

  • Definition 1: Metric over Functions editdistance
  • Proposition 2
  • Proposition 3: editdistance
  • Definition 4: Twinning Property (TP)
  • Definition 5: Approximate Twinning Property (ATP)
  • Definition 6: Strongly Connected Twinning Property (STP)
  • Definition 7: Hamming Twinning Property (HTP)
  • Proposition 8
  • Lemma 9
  • Lemma 11
  • ...and 22 more