Deciding equivalence of regular languages

Given two regular expressions $R$ and $S$ on an alphabet $\Sigma$ it is possible to decide their equivalence as follows:

1. build two finite automata $M_R$ and $M_S$ such that $L(R) = L(M_R)$ and $L(S) = L(M_S)$
2. build an automaton $M$ such that $L(M) = (L(M_R) - L(M_S)) \cup (L(M_S) - L(M_R))$
3. test emptyness of $L(M)$ using a reachability algorithm on $M$

I was wondering if there is another way to decide equivalence. Suppose $M_R$ and $M_S$ are the minimal DFA (without epsilon-moves) such that $L(R) = L(M_R)$ and $L(S) = L(M_S)$. If they have a different number of states, then $R$ and $S$ are not equivalent. Otherwise let $m$ be the number of states of the two automata. Is it true that $L(M_R) = L(M_S)$ iff $\{x \in L(M_R) : |x| \leq m +1 \} = \{x \in L(M_S) : |x| \leq m +1 \}$? How to prove that with the Myhill-Nerode theorem?

• This question might be a better fit for cs.SE. – Snowball Sep 11 '12 at 14:19
• For what it's worth, I think your idea is plausible (although I think you can reduce the $m+1$ to just $m$) and probably does follow from the Myhill-Nerode theorem. I will try to think about it more carefully in the next day or two. – MJD Sep 12 '12 at 2:25

Here is a concrete counterexample to the conjecture, now that I’m reading it correctly.

Let $R=(a\lor b)^3\Big(a(a\lor b)^5\Big)^*$ and $S=(a\lor b)^3\Big(b(a\lor b)^5\Big)^*$. These have the $7$-state DFAs whose transitions tables are shown below; $s_0$ is the initial state, and $s_3$, shown in red, is the sole acceptor state.

$$\begin{array}{r|cc} M_R&a&b\\ \hline s_0&s_1&s_1\\ s_1&s_2&s_2\\ s_2&\color{red}{s_3}&\color{red}{s_3}\\ \color{red}{s_3}&s_4&s_6\\ s_4&s_5&s_5\\ s_5&s_0&s_0\\ s_6&s_6&s_6 \end{array} \qquad\qquad \begin{array}{r|cc} M_S&a&b\\ \hline s_0&s_1&s_1\\ s_1&s_2&s_2\\ s_2&\color{red}{s_3}&\color{red}{s_3}\\ \color{red}{s_3}&s_6&s_4\\ s_4&s_5&s_5\\ s_5&s_0&s_0\\ s_6&s_6&s_6 \end{array}$$

The eight words of length $3$ are the only words of length at most $8$ in both $L(M_R)$ and in $L(M_S)$, but the languages are not the same: $a^9\in L(M_R)\setminus L(M_S)$.

The problem is that the minimal redundant loop $s_3\to s_4\to s_5\to s_0\to s_1\to s_2\to s_3$ is too long and its starting point too far removed from the initial state, so the difference in the two languages doesn’t show up within the first $8$ transitions.

• @MJD: Because I ‘saw’ cardinality signs that weren’t there. – Brian M. Scott Sep 12 '12 at 1:16
• @MJD: exactly, you're right. I thought about it but I never heard or read of this property at university or in a book. However the bound cannot be $m+1$. There is Brian's counterexample and also this other one. Let $m>1$ be a natural number and define $L_1=\{a^n : n \text{ not multiple of } m \}$ and $L_2=\{a^n : n \geq 1,\ n \neq m \}$. Both have a minimal $m+2$ states DFA. Indeed $\{x \in L_1 : |x|<2m\}=\{x \in L_2:|x|<2m\}$ but $L_1 \neq L_2$. – Alberto Sep 13 '12 at 9:36
• [I mistakenly deleted this comment, which is the one to which the two previous comments are referring.] I don't see why you think OP is trying to compare the number of words of each length. It appears to me that OP's idea was that one can reduce the question of comparing the infinite sets $L_1$ and $L_2$ to the finite question of comparing the finite subsets of $L_1$ and $L_2$ that consist of just the words of length at most $m+1$. – MJD Sep 13 '12 at 22:14

Theorem Let $\mathcal{A}$ and $\mathcal{B}$ be two DFA's with $m$ states and $n$ states, respectively. Then $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{B})$ iff $\{x \in \mathcal{L}(\mathcal{A}) : |x| < mn \} = \{x \in \mathcal{L}(\mathcal{B}) : |x| < mn \}$.

Proof We prove the two directions of the double implication.

($\Rightarrow$) Trivial.

($\Leftarrow$) We prove the contrapositive. Suppose $\mathcal{L}(\mathcal{A}) \neq \mathcal{L}(\mathcal{B})$ and let $w$ be a word of minimal lenght such that $w \not\in \mathcal{L}(\mathcal{A}) \cap \mathcal{L}(\mathcal{B}) = \mathcal{L}(\mathcal{A} \times \mathcal{B})$. Suppose, by way of contradiction, that $|w| \geq mn$. We set $X = \{\hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,x) : x \text{ prefix of } w\}$. Since $|X| \geq mn+1$ and $|Q_{\mathcal{A}\times\mathcal{B}}| = mn$, there exist two prefixes $u,u'$ of $w$ such that $\hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,u) = \hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,u')$. We can assume w.l.o.g. that $u$ is a prefix of $u'$. Hence there exist two strings $v,z$ such that $uv = u'$ and $u'z = w$ and hence $uvz = w$. Moreover since $u \neq u'$, the string $v$ is non-trivial, (i.e. $|v| \geq 1$). Now note that $\hat{\delta}_{\mathcal{A} \times \mathcal{B}}(\hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,u),v) = \hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,u)$, i.e. the characters composing the string $v$ lead the automaton $\mathcal{A} \times \mathcal{B}$ through a loop from the state $\hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,u)$ into itself. Therefore the string $uz$ is such that $\hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,uz) = \hat{\delta}_{\mathcal{A} \times \mathcal{B}}(q_0,w)$ and $|uz|<|w|$. This contradicts the minimality of $w$.

• The theorem above gives an alternative effective way of deciding equivalences of regular languages. – Alberto Sep 12 '12 at 13:36
• Is there a source for this theorem? – Takkun Sep 12 '12 at 22:08
• No. But the proof is easily derived from the proof of Pumping Lemma for Regular Languages – Alberto Sep 13 '12 at 9:28
• I think you can find an algorithm based on this idea in Hopcroft and Ullman. – Kaveh Sep 17 '12 at 5:34

I have not read this paper, "Testing the Equivalence of Regular Languages", by Almeida, Moreira, and Reis, but the abstract sounds quite promising:

Antimirov and Mosses presented a rewrite system for deciding the equivalence of two (extended) regular expressions and argued that this method could lead to a better average-case algorithm than those based on the comparison of the equivalent minimal DFAs. In this paper we present a functional approach of a variant of that method, prove its correctness and give some experimental comparative results. Although being a refutation method, our preliminary results lead to the conclusion that indeed this method is feasible and it is, almost always, faster than the classical methods.

• I made this community-wiki mode because it is not at all an answer to the question you asked. – MJD Sep 11 '12 at 14:08