MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

4 fixed a misstatement

If $M_R$ and $M_S$ have $m,n$ states respectively, then one has that $L(M_R)=L(M_S)$ iff they have the same words of length at most $mn-1$. This is essentially the content of your algorithm. Suppose that they are different and let $w$ be a minimal length word accepted by one of the machines and not the other. If $w$ has length greater than $mn-1$, then when you run $w$ from the initial state of $M_R\times M_S$, you will get a loop. This loop will give you a factorization $w=xuy$ where $u$ reads a loop in both $M_R$ and $M_S$. So then $xy$ will be accepted in one of the machines and not the other and have smaller length.

I don't think your proposed bound would work but I have to think a little to get an example.

Added. I believe this is a counter example. Let m be an integer. Consider over a unary alphabet the languages $R=\lbrace 1,a,..,a^{m-3},a^{m-1}\rbrace^*$ a^n\mid n\not\equiv m-2 \pmod m\rbrace$and$S=\lbrace 1,a,..,a^{m-3}\rbrace\cup \lbrace a^n\mid n\geq m-1\rbrace$. Then both of these are recognized by an$m$-state automaton (I believe both are minimal) and the shortest word in one, but not the other, is$a^{m-1}a^{m-1}=a^{2m-2}$, a^{2m-2}$, which has length $2m-2$. I hope this works.

3 added 449 characters in body; added 4 characters in body; edited body; edited body

If $M_R$ and $M_S$ have $m,n$ states respectively, then one has that $L(M_R)=L(M_S)$ iff they have the same words of length at most $mn-1$. This is essentially the content of your algorithm. Suppose that they are different and let $w$ be a minimal length word accepted by one of the machines and not the other. If $w$ has length greater than $mn-1$, then when you run $w$ from the initial state of $M_R\times M_S$, you will get a loop. This loop will give you a factorization $w=xuy$ where $u$ reads a loop in both $M_R$ and $M_S$. So then $xy$ will be accepted in one of the machines and not the other and have smaller length.

I don't think your proposed bound would work but I have to think a little to get an example.

Added. I believe this is a counter example. Let m be an integer. Consider over a unary alphabet the languages $R=\lbrace 1,a,..,a^{m-3},a^{m-1}\rbrace^*$ and $S=\lbrace 1,a,..,a^{m-3}\rbrace\cup \lbrace a^n\mid n\geq m-1\rbrace$. Then both of these are recognized by an $m$-state automaton (I believe both are minimal) and the shortest word in one, but not the other, is $a^{m-1}a^{m-1}=a^{2m-2}$, which has length $2m-2$. I hope this works.

2 added 3 characters in body

If $M_R$ and $M_S$ have $m,n$ states respectively, then one has that $L(M_R)=L(M_S)$ iff they have the same words of length at most $mn-1$. This is essentially the content of your algorithm. Suppose that they are different and let $w$ be a minimal length word accepted by one of the machines and not the other. If the length $w$ has length greater than $mn-1$, then when you run $w$ from the initial state of $M_R\times M_S$, you will get a loop. This loop will give you a factorization $w=xuy$ where $u$ reads a loop in both $M_R$ and $M_S$. So then $xy$ will be accepted in one of the machines and not the other and have smaller length.

I don't think your proposed bound would work but I have to think a little to get an example.

1