== Проверка ДКА на эквивалентность ==
Заданы два автомата: <tex> \mathcal{A}_1 </tex> со стартовым состоянием <tex> s_1 </tex> и <tex> \mathcal{A}_2 </tex> со стартовым состоянием <tex> s_2 </tex> соответственно. Нужно проверить их на эквивалентность.
'''Замечание:''' для реализации оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские состояния]].
=== Проверка через минимизацию ===
Для этого построим автомат <tex> \mathcal{A} </tex>, содержащий все состояния обоих автоматов и изначальные переходы между ними. Стартовым состоянием в новом автомате можно сделать <tex> s_1 </tex> или <tex> s_2 </tex> — это не имеет значения. При этом состояния одного из автоматов станут недостижимыми из новый стартовой вершины в новом автомате, но для алгоритма это и не важно.<br>
Также можно минимизировать каждый автомат отдельно и проверить минимизированные версии на изоморфизм.
Замечание: для реализации оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские состояния]].
=== Проверка через BFS ===
Алгоритм заключается Два автомата можно также проверить на эквивалентность, используя [[Обход в синхронном обходе автоматов ширину | обход в ширину]]. Будем синхронно обходить два автомата, проверяяначиная со стартовых состояний, что по пути сохраняются терминальные состояния.Поскольку '''эквивалентные''' автоматы '''допускают''' один тот же язык, при переходе по одним и тем же символам в обоих автоматахпоисках такой строки, слово должно приниматься обоими автоматами одновременнокоторая различает два состояний этих автоматов. То есть вершины, в которые мы перешли, должны быть либо одновременно '''терминальными''', либо одновременно '''нетерминальными'''она будет допускаться одним автоматом, что и проверяет приведённый алгоритмно не будет принадлежать языку другого.
Поскольку эквивалентные автоматы допускают один тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, либо одновременно нетерминальными, что и проверяет приведённый алгоритм.
==== Псевдокод ====
<wikitex>
Псевдокод: <font color=green>// <tex>Q</tex> $\mathtt{aut}[i][c]$ {{---}} очередь номер состояния, в которое есть переход из пар состоянийсостояния $i$ по символу $c$</font> '''boolean'' '''function''' $\mathtt{bfsEquivalenceCheck}$($\mathtt{aut1}$: '''int[][]''', $\mathtt{aut2}$: '''int[][]'''): $Q.\mathtt{push}( \langle s_1, s_2 \rangle ) $<font color=green>// <tex>Q</tex> {{---}} очередь из пар состояний</font> $\mathtt{used1}[s_1]} \leftarrow $ ''true'' $\mathtt{used2}[s_2]} \leftarrow $ ''true'' '''while''' $Q \ne \varnothing $ $u \leftarrow Q.front.first$ $, v \leftarrow Q.front.second$ $\mathtt{Q.pop}()}$ '''if'''( $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$ )
'''return''' ''false''
'''for''' $i c \in \Sigma$ '''if'''( '''not''' $\mathtt{used1[aut1}[u][ic]]}$ || '''or''' '''not''' $\mathtt{used2[aut2}[v][ic]]} $) $Q.\mathtt{push}( \langle \mathtt{aut1}[u][ic]}, \mathtt{aut2}[v][ic]} \rangle )$ $\mathtt{used1[aut1}[u][ic]]} \leftarrow $ ''true'' $\mathtt{used2[aut2}[v][ic]]} \leftarrow $ ''true'' '''return''''' true;''</wikitex>Корректность алгоритма следует из строго доказательства того факта, что если два состояния $u$ и $v$ различаются какой-то строкой, то они различаются строкой длины $O(n)$.
ЗамечаниеИнтуитивное понимание алгоритма такое: пусть по строке $w$ мы пришли в данной реализации состояния $ \langle u, v \rangle $, и пусть они оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские нетерминальные. После этого совершим переход по символу $c$ в состояния]]$ \langle u', v' \rangle $.
<wikitex>Доказательство корректности:Пусть по строке $w$ мы пришли в состояния $ \langle u, v \rangle $, и пусть они нетерминальные. Пусть мы перешли по символу $c$ в состояние $ \langle u', v' \rangle $ ($u$ может быть равно $u'$ или $v'$ может быть равно $u'$, но не оба сразу). Тогда если $\mathtt{isTerminal1[u']} \ne \mathtt{isTerminal2[v']}$, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны.
</wikitex>
