# (Symbolic) Equivalence of deterministic infinite word transducers with restriction

Given a deterministic infinite word transducer (also called deterministic generalized sequential machine) with the following restriction:

• There is exactly one initial state
• All states are final
• The transducer is real-time, i.e. reads excactly one input character on each transition
• The transducer produces zero or more output characters on each transition
• The deterministic input automaton (obtained by eliminating the output on each transition) recognizes $\Sigma^\omega$, i.e. each state has $|\Sigma|$ transitions, one for each input character
• There are no output $\epsilon$-loops, i.e. any infinite path yields an infinite word output

Are there special algorithms to decide equivalence for this type of automaton? I am particularly interested in those algorithms that admit a symbolic solution, e.g. using an SMT solver.

Note that one way to decide equivalence of two such transducers is to decide if the union of both automata is single-valued. However, I am not aware of a symbolic algorithm to decide single-valuedness if both states and transitions are given symbolically (e.g. by bit-vector constraints).