Working Seminar on Formal Models, Discrete Structures, and Algorithms

Streaming string transducers

Pavol Černý (IST Austria)

When: April 18, 2pm

Where: room G2.91b


We introduce streaming string transducers that map input strings to output strings in a single left-to-right pass. The transducer uses a finite set of states, and a finite set of variables ranging over strings. At every step, it can make decisions based on the next input symbol, updating its state, and updating string variables by concatenating string variables and new symbols from the output alphabet. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over input/output strings, are in PSPACE. There is a robust and well-studied class of ``regular'' transductions on finite alphabets. This class of transductions can be defined by two-way deterministic finite-state transducers and it has a logical MSO-based characterization. We establish that the streaming string transducers capture exactly the class of regular transductions.

For applications to program verification, we define data streaming string transducers (DSSTs) that operate on data strings. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain that supports only the operations of equality and ordering. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to DSSTs. The imperative programs dynamically modify a singly-linked heap by changing next-pointers of heap-nodes and by adding new nodes. The main restriction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.

This is joint work with Rajeev Alur.