Поскольку '''эквивалентные''' автоматы '''допускают''' один тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно '''терминальными''', либо одновременно '''нетерминальными''', что и проверяет приведённый алгоритм.
<wikitex>
Псевдокод:
bfs_equivalence_check<font color=green>// <tex>Q</tex> {{---}} очередь из пар состояний</font> '''function''' $\mathtt{bfsEquivalenceCheck}$($aut1$, $aut2$) '''$\mathtt{insert''' <tex>} \{langle s_1, s_2\}</tex> rangle in <tex>Q </tex>$ $\mathtt{used1[0] <tex> } \leftarrow </tex> $ ''true;'' $\mathtt{used2[0] <tex> } \leftarrow </tex> $ ''true;'' '''while''' <tex>$Q \ne \varnothing </tex> $ $u <tex> \leftarrow </tex> Q.front.first;$ $v <tex> \leftarrow </tex> Q.front.second;$ $\mathtt{pop(Q);}$ '''if'''($\mathtt{isTerminal1[u] != } \ne \mathtt{isTerminal2[v]}$ ) '''return''''' false;'' '''for''' <tex>$i \in \Sigma</tex>$ '''if'''(!'''not''' $\mathtt{used1[aut1[u][i]] }$ || ! '''not''' $\mathtt{used2[aut2[v][i]]} $) '''insert''' <tex>$ \langle \mathtt{</tex>aut1[u][i]}, \mathtt{aut2[v][i]<tex>} \rangle \}</tex> in <tex>Q</tex>$ $\mathtt{used1[aut1[u][i]] <tex> } \leftarrow </tex> $ ''true;'' $\mathtt{used2[aut2[v][i]] <tex> } \leftarrow </tex> $ ''true;''
'''return''' true;
</wikitex>
Замечание: в данной реализации оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские состояния]].
