Nondeterministic Streaming String Transducers

We introduce

nondeterministic streaming string transducers

(

nssts

) – a new computational model that can implement MSO-definable relations between strings. An

nsst

makes a single left-to-right pass on the input string and uses a finite set of

string variables

to compute the output. In each step, it reads one input symbol, and updates its string variables in parallel with a

copyless assignment

. We show that

nsst

are closed under sequential composition and that their expressive power coincides with that of nondeterministic MSO-definable transductions. Further, we identify the class of

functional

nssts

; such an

nsst

allows nondeterministic transitions, but for every successful run on a given input generates the same output string. We show that deciding functionality of an arbitrary

nsst

is decidable with

pspace

complexity, while the equivalence problem for functional

nssts

is

pspace-complete

. We also show that checking if the set of outputs of an

nsst

is contained within the set of outputs of a finite number of

dssts

is decidable in

pspace

.