Regular Transformations of Infinite Strings

The theory of regular transformations of finite strings is quite mature with appealing properties. This class can be equivalently defined using both logic (Monadic second-order logic) and finite-state machines (two-way transducers, and more recently, streaming string transducers); is closed under operations such as sequential composition and regular choice; and problems such as functional equivalence and type checking, are decidable for this class. In this paper, we initiate a study of transformations of infinite strings. The MSO-based definition for regular string transformations generalizes naturally to infinite strings. We define an equivalent generalization of the machine model of streaming string transducers to infinite strings. A streaming string transducer is a deterministic machine that makes a single pass over the input string, and computes the output fragments using a finite set of string variables that are updated in a copyless manner at each step. We show how Muller acceptance condition for automata over infinite strings can be generalized to associate an infinite output string with an infinite execution. The proof that our model captures all MSO-definable transformations uses two-way transducers. Unlike the case of finite strings, MSO-equivalent definition of two-way transducers over infinite strings needs to make decisions based on omega-regular look-ahead. Simulating this look-ahead using multiple variables with copyless updates, is the main technical challenge in our constructions. Finally, we show that type checking and functional equivalence are decidable for MSO-definable transformations of infinite strings.