Algorithmic Verification of Single-Pass List Processing Programs

We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. 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. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next input symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenating data-string variables and new symbols formed from data variables, while avoiding duplication. We establish PSPACE bounds for the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by ...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Rajeev Alur, Pavol Cerný
• Keywords: CORR 2010, Data Strings, Education, Finite Set, Transducers