Edit Distance of Finite-Valued Transducers

Technical Summary: Edit Distance of Finite-Valued Transducers

Problem Statement
The paper addresses the computability of the edit distance between two finite-state transducers. While the edit distance between functional transducers (where each input maps to at most one output) is known to be computable, the problem is generally uncomputable for arbitrary transducers. The authors investigate whether this computability extends to the class of finite-valued transducers, where each input word maps to at most $k$ output words for a fixed constant $k$. This class is strictly more expressive than functional transducers but retains decidability for many fundamental problems (e.g., inclusion and equivalence) that are undecidable in the general case.

Methodology
The proposed solution proceeds through a reduction strategy that transforms the problem of computing the distance between finite-valued transducers into a series of computable sub-problems involving sequential transducers and a newly introduced metric concept.

1. Reduction to Multi-Sequential Transducers:
   The authors leverage the known result that any finite-valued transducer can be effectively decomposed into a finite union of unambiguous (and thus functional) transducers. They construct a product automaton that synchronizes the runs of all component transducers of two given finite-valued transducers, $T$ and $S$. This construction yields two multi-sequential transducers, $T'$ and $S'$ (finite unions of sequential/deterministic transducers), such that the edit distance $d(T, S)$ is preserved and equal to $d(T', S')$.

2. Introduction of Relative Distance:
   To compute the distance between multi-sequential relations (which are unions of sequential functions), the authors introduce the concept of relative distance. The relative distance from a function $f$ to a relation $R$, denoted $\vec{d}(f, R)$, is defined as the supremum over all inputs $u$ of the minimal edit distance between $f(u)$ and some $v \in R(u)$.
   The distance between two multi-sequential relations $R = \bigcup f_i$ and $S = \bigcup g_j$ is shown to be the maximum of the relative distances between each component function and the opposing relation:
   $$d(R, S) = \max \left( \max_i \vec{d}(f_i, S), \max_j \vec{d}(g_j, R) \right)$$

3. Decidability of Relative Distance:
   The computability of the relative distance $\vec{d}(f, R)$ is established by reducing it to two boundedness problems:

   • Finiteness: Deciding if $\vec{d}(f, R) < \infty$.

   • $k$-Finiteness: Deciding if $\vec{d}(f, R) \leq k$ for a given integer $k$.

   • Finiteness Check: The authors construct a product transducer $T$ representing the synchronous runs of $f$ and the components of $R$. They partition the domain of $f$ based on which components of $R$ accept the input. For each partition, they analyze the strongly connected components (SCCs) of the product transducer. Using properties of word conjugacy (specifically, that infinite bounded edit distance implies conjugacy of loop outputs), they prove that the relative distance is finite if and only if, for every path of SCCs in the product, there exists at least one component relation whose output loop is conjugate to the function's output loop. This reduces the problem to checking the finiteness of the distance between sequential transducers, which is decidable.

   • $k$-Finiteness Check: To decide if the distance is bounded by $k$, the authors construct a non-deterministic finite automaton (NFA), $A_{C,k}$, that tracks the edit budget and "leftover" unmatched suffixes between the function's output and the relation's outputs. The relative distance is $\leq k$ if and only if the language accepted by $A_{C,k}$ is identical to the domain of the product transducer.

Key Contributions and Results

• Main Theorem: The edit distance between two finite-valued rational relations is computable for metrics in the Levenshtein family (Levenshtein, Longest Common Subsequence, and Damerau-Levenshtein).
• Algorithmic Framework: The paper provides a constructive procedure to compute this distance by reducing the finite-valued case to the multi-sequential case, and subsequently to the relative distance between a sequential function and a multi-sequential relation.
• Complexity Analysis: The authors note that their procedure results in a 3-EXPSPACE upper bound. This arises from the exponential space required to convert finite-valued transducers to multi-sequential ones, followed by exponential and doubly exponential space requirements for the subsequent relative distance computations. The lower bound is at least PSPACE-hard, as it subsumes the equivalence problem for non-deterministic automata.

Significance and Claims
The paper claims to extend the known decidability of edit distance beyond functional transducers to the broader class of finite-valued transducers. This is significant because finite-valued transducers strike a balance between expressive power and algorithmic tractability, capturing many practical scenarios where a single input may yield a small, bounded set of valid outputs (e.g., in natural language processing or program synthesis).

The authors emphasize that their work provides a foundation for approximate reasoning in reactive systems. In classical verification, a system is checked for exact conformance to a specification. The concept of relative distance allows for reasoning about systems that are "close" to a specification, accommodating minor deviations. The paper does not claim to optimize the algorithm for efficiency, acknowledging the high complexity, but asserts that the result establishes the theoretical possibility of computing these distances in a practically motivated, expressive class of transducers. The techniques are also noted to be adaptable to other edit metrics, such as Hamming distance, with minor modifications.