Expressiveness of streaming string transducers

10 years 10 months ago
Expressiveness of streaming string transducers
Streaming string transducers [1] define (partial) functions from input strings to output strings. A streaming string transducer makes a single pass through the input string and uses a finite set of variables that range over strings from the output alphabet. At every step, the transducer processes an input symbol, and updates all the variables in parallel using assignments whose right-hand-sides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a right-hand-side expression. It has been shown that streaming string transducers operating on strings over infinite data domains are of interest in algorithmic verification of list-processing programs, as they lead to Pspace decision procedures for checking pre/post conditions and for checking semantic equivalence, for a well-defined class of heap-manipulating programs. In order to understand the theoretical expressiveness of streaming transducers, we focus on streaming transduce...
Rajeev Alur, Pavol Cerný
Added 11 Feb 2011
Updated 11 Feb 2011
Type Journal
Year 2010
Authors Rajeev Alur, Pavol Cerný
Comments (0)