10.4230/LIPICS.FSTTCS.2010.1
Alur, Rajeev
Rajeev
Alur
Černý, Pavol
Pavol
Černý
Expressiveness of streaming string transducers
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Article
streaming string transducer
list processing
heap manipulation
monadic second-order transduction
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
2010
2010-12-14
2010-12-14
2010-12-14
en
urn:nbn:de:0030-drops-28538
10.4230/LIPIcs.FSTTCS.2010
978-3-939897-23-1
1868-8969
10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS 2010
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
2013
8
1
1
12
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
8
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
492344 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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 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/postconditions 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 transducers processing strings over finite alphabets, given the existence of a robust and well-studied class of ``regular'' transductions for this case. Such regular transductions can be defined either by two-way deterministic finite-state transducers, or using a logical MSO-based characterization. Our main result is that the expressiveness of streaming string transducers coincides exactly with this class of regular transductions.
LIPIcs, Vol. 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 1-12