Alur, Rajeev ;
Černư, Pavol
Expressiveness of streaming string transducers
Abstract
Streaming string transducers 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 righthandsides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a righthandside expression. It has been shown that streaming string transducers operating on strings over infinite data domains are of interest in algorithmic verification of listprocessing programs, as they lead to Pspace decision procedures for checking pre/postconditions and for checking semantic equivalence, for a welldefined class of heapmanipulating programs. In order to understand the theoretical expressiveness of streaming transducers, we focus on streaming transducers processing strings over finite alphabets, given the existence of a robust and wellstudied class of ``regular'' transductions for this case. Such regular transductions can be defined either by twoway deterministic finitestate transducers, or using a logical MSObased characterization. Our main result is that the expressiveness of streaming string transducers coincides exactly with this class of regular transductions.
BibTeX  Entry
@InProceedings{alur_et_al:LIPIcs:2010:2853,
author = {Rajeev Alur and Pavol Čern{\'y}},
title = {{Expressiveness of streaming string transducers}},
booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
pages = {112},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897231},
ISSN = {18688969},
year = {2010},
volume = {8},
editor = {Kamal Lodaya and Meena Mahajan},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2853},
URN = {urn:nbn:de:0030drops28538},
doi = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.1},
annote = {Keywords: streaming string transducer, list processing, heap manipulation, monadic secondorder transduction}
}
2010
Keywords: 

streaming string transducer, list processing, heap manipulation, monadic secondorder transduction 
Seminar: 

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Issue date: 

2010 
Date of publication: 

2010 