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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.