Equivalence of Deterministic Top-Down Tree Transducers is ExpTime-Complete

The class of Deterministic Top-Down Tree Transducers (DTOP) has been studied for a long time, but while its equivalence problem was known to be ExpTime-Hard, the best known algorithms were coNExpTime (search of counter-example) or 2ExpTime (full normalization).
The exact complexity bound is of relevance, as some classes that extends DTOP (lookahead, symbolic) have an equivalence problem that efficiently reduces to DTOP equivalence.
In this talk we will see an ExpTime algorithm for DTOP equivalence, derived from an algorithm that decides functionality of nondeterministic one-way word transducers.