Foundations of Finite Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner · 2011
Finite transducers on trees are fundamental to computer science. They form the basis of many applications that manipulate strings and trees. The conventional representation of finite transducers assume a finite set of states and a finite alphabet. Classical algorithms and representations make essential use of both of these assumptions. In many cases, the complexity of the algorithms is computed based on the number of states and alphabet size. But how important are these assumptions really for the main operations and decision problems? We have recently pursued applications of finite transducers in the context of web security as a foundation for sanitization of potentially malicious data. For these applications we have found that lifting the finite alphabet restriction to be useful to enable efficient symbolic analysis and we have developed symbolic counter-parts of the main classical operations on finite automata. We here define Symbolic Tree Transducers as a generalization of Regular Transducers as finite state input-output tree automata with logical constraints over a background theory. The background theory Microsoft Research, Redmond, WA, USA{margus,nbjorner}@microsoft.comis a parameter of the formalization. We examine key closure properties of Symbolic Tree Transducers and we develop a composition algorithm and an equivalence decision procedure for single-valued transducers.