The “Hilbert Method” for Solving Transducer Equivalence Problems

The "Hilbert Method" applies classical results from algebraic geometry, e.g. Hilbert's Basis Theorem, to prove decidability of equivalence on certain classes of transducers.

In the first part, following [1], we will describe the method and sketch the proof of correctness.

In the second part, we will present new results [2], concerning decidability of equivalence:

1. Positive result on MSO-definable transformations on Unordered Forests.
2. Negative result on a class more general than Macro Tree Transducers.

[1] "Automata Toolbox", Bojańczyk, M., Czerwiński, W.
[2] "The “Hilbert Method” for Solving Transducer Equivalence Problems", Boiret. A., Piórkowski, R., S.