Determining if transducer automaton has two states with intersecting images, without minimizing?

I work (in implementation!) with deterministic finite state automata with input and output; i.e. there are transitions (start state,input letter)$$\to$$(new state,output letter). Thus every state gives a transformation {words}$$\to$${words}.

I want to determine whether there exist two states which act identically on arbitrarily long words. Formally, consider the coarsest relation $$\sim$$ on the stateset such that $$x\sim y$$ iff there are letters $$a,b$$ and transitions $$(x,a)\to(x',b)$$ and $$(y,a)\to(y',b)$$ with $$x'\sim y'$$. I want to know if there is $$x\neq y$$ with $$x\sim y$$.

I can do this by composing the transducer with its transpose (switching input and output), minimizing, intersecting with the diagonal on the alphabet, and detecting whether a state $$(x,y)$$ in the product of states survives with $$x\neq y$$.

However, I'd very much like a faster algorithm, say of complexity $$O(n\log n)$$ with $$n=$$ number of states (the alphabet size can be assumed small).

I thought about adapting Hopcroft's (1971) algorithm, by constructing a partition of the stateset in which, initially, two states $$x,y$$ are in the same part iff there exists a letter $$a$$ with $$(x,a)\to(x',b)$$ and $$(y,a)\to(y',b)$$ for some $$x',y'$$, and then refining the partition; however it doesn't seem to work straight off the bat.

EDIT: here is more explicitly the relation I am interested in. Say two states $$x,y$$ in a transducer are weakly equivalent, $$x\sim y$$, if there is at least one letter $$a$$ such that $$x,y$$ have the same output on input $$a$$, and lead to weakly equivalent respective states. This defines uniquely weak equivalence if one asks for $$\sim$$ to be maximal with this property. (Beware that it is not, in general, and equivalence relation).

It may be computed as follows: start by $$x\sim_0 y$$ for all $$x,y$$; then define $$x\sim_n y$$ if there is a letter $$a$$ and transitions $$(x,a)\to(x',b)$$ and $$(y,a)\to(y',b)$$ with $$x'\sim_{n-1}y'$$. These are a descending sequence of relations, so must stabilize, and they stabilize to weak equivalence.

The real question I'm interested in is not how to compute $$\sim$$, but merely to determine whether it is non-trivial; and I want to do that in subquadratic time, ideally linear up to logarithmic terms.

• Apparently there are previous works on minimizing transducers. See e.g. this post. Have you studied them already? If so, what have you found, and how does it fall short for your purpose? Even if all of the full minimization algorithms are too slow for your purpose, they may use some ideas that would help. Also, what is known about the analogous problem for ordinary DFAs? One of the answers at that link suggests your problem might reduce to that problem (if your transducer has no epsilon transitions). Jun 4, 2020 at 19:08
• Looking further, Breslauer 1998 Theorem 4.1 seems to claim a nearly linear-time algorithm for full minimization. See also Cho'rut 2003, page 142. Do any of those help? Jun 4, 2020 at 19:32
• Hi @NealYoung! There is no issue on what minimization means, my automata are deterministic, so the classical Hopcroft algorithm runs in $O(n \log n)$ worst-case time, an even $O(n \log \log n)$ average. However, if I first multiply the automaton with itself, I'm up to $O(n^2)$ even ignoring the logarithmic terms. Said differently, I define an equivalence relation in my post. It's not equivalence of states, but something coarser. Can it be computed in subquadratic time? The algorithm I sketched to compute it is necessarily worse than quadratic....
– grok
Jun 4, 2020 at 20:57
• ... Your links are welcome, but only if one reduces from my relation to state equivalence, and then one already goes beyond quadratic.
– grok
Jun 4, 2020 at 21:02
• It's weird that you define your relation with "there exists a letter a". Then according to this, two states will be equivalent if there exists a long word on which they behave the same, but their behaviour might differ on other words. Jun 5, 2020 at 11:10