FO-definable transformations of infinite strings

TL;DR

This paper extends the theory of regular and aperiodic string transformations from finite to infinite strings, establishing logical and automata-theoretic equivalences for first-order definable transformations over infinite strings.

Contribution

It generalizes existing finite string transformation results to infinite strings, connecting first-order logic, aperiodic transducers, and streaming string transducers for infinite strings.

Findings

Established equivalence between FO-definable transformations and aperiodic transducers for infinite strings.

Extended the connection between logical definability and automata models to the infinite string setting.

Provided a framework for analyzing transformations of infinite strings using logical and automata-theoretic tools.

Abstract

The theory of regular and aperiodic transformations of finite strings has recently received a lot of interest. These classes can be equivalently defined using logic (Monadic second-order logic and first-order logic), two-way machines (regular two-way and aperiodic two-way transducers), and one-way register machines (regular streaming string and aperiodic streaming string transducers). These classes are known to be closed under operations such as sequential composition and regular (star-free) choice; and problems such as functional equivalence and type checking, are decidable for these classes. On the other hand, for infinite strings these results are only known for $\omega$-regular transformations: Alur, Filiot, and Trivedi studied transformations of infinite strings and introduced an extension of streaming string transducers over $\omega$-strings and showed that they capture monadic second-order definable transformations for infinite strings. In this paper we extend their work to recover connection for infinite strings among first-order logic definable transformations, aperiodic two-way transducers, and aperiodic streaming string transducers.