Finite-valued Streaming String Transducers

A transducer is finite-valued if there exists a bound 𝑘 such that any given input maps to at most 𝑘 outputs. For classical one-way transducers, it is known since the 1980s that finite valuedness entails decidability of the equivalence problem. This result is in contrast with undecidability in the general case, making finite-valued transducers very appealing. For one-way transducers it is also known that finite valuedness itself is decidable and that any 𝑘-valued finite transducer can be decomposed into a union of 𝑘 single-valued finite transducers. In this article, we extend the above results to copyless streaming string transducers (SSTs), addressing open questions raised by Alur and Deshmukh in 2011. SSTs strictly extend the expressiveness of one-way transducers via additional variables that store partial outputs. We prove that any 𝑘-valued SST can be effectively decomposed into a union of 𝑘 (single-valued) deterministic SSTs. As a corollary, we establish the equivalence between SSTs and two-way transducers in the finite-valued case, even though these models are generally incomparable.

Another corollary provides an elementary upper bound for deciding equivalence of finite-valued SSTs. The equivalence problem was already known to be decidable, but the proof complexity relied on Ehrenfeucht's conjecture. Lastly, our main contribution shows that finite valuedness of SSTs is decidable, with the complexity being PSpace in general, and PTime when the number of variables is fixed.