Reversible Transducers over Infinite Words

TL;DR

This paper extends the concept of reversible two-way transducers to infinite words, demonstrating they have the same expressive power as deterministic transducers and enabling efficient composition with polynomial complexity.

Contribution

It introduces reversible two-way transducers over infinite words and proves they are as expressive as deterministic transducers, with efficient polynomial composition.

Findings

Reversible two-way transducers over infinite words have the same expressiveness as deterministic ones.

Composition of reversible transducers over infinite words is polynomial in complexity.

Effective construction induces a single exponential state blow-up.

Abstract

Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to reactive synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. An important result by Dartois et al. shows that composition of two-way transducers enjoy a polynomial composition when the underlying transducer is reversible, that is, if they are both deterministic and co-deterministic. This is a major improvement over general deterministic two-way transducers, for which composition causes a doubly exponential blow-up in the size of the inputs in general. Moreover, they show that reversible two-way transducers have the same expressiveness as deterministic two-way transducers. However, the question of expressiveness of reversible transducers over infinite words is still open. In this article, we introduce the class of reversible two-way transducers over infinite words and show that they enjoy the same expressive power as deterministic two-way transducers over infinite words. This is done through a non-trivial, effective construction inducing a single exponential blow-up in the set of states. Further, we also prove that composing two reversible two-way transducers over infinite words incurs only a polynomial complexity, thereby providing foundations for efficient procedure for composition of transducers over infinite words.