On the expressiveness of deterministic transducers over infinite trees

Abstract. We introduce top-down deterministic transducers with ra-tional lookahead (transducer for short) working on innite terms. We show that for such a transducer eT, there exists an MSO-transduction T such that for any graph G, unfold(T (G)) = eT (unfold(G)). Recipro-cally, we show that if an MSO-transduction T \preserves bisimilarity", then there is a transducer eT such that for any graph G, unfold(T (G)) = eT (unfold(G)). According to this, transducers can be seen as a complete method of implementation of MSO-transductions that preserve bisimi-larity. One application is for transformations of equational systems.