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).