Изменения

Пусть язык содержит слово <tex>w</tex>. Любой [[Детерминированные конечные автоматы| детерминированный конечный автомат ]] <tex>A</tex>, задающий этот язык, должен допускать <tex>w</tex>. Тогда при переходе из стартового состояния <tex>A</tex> по символам <tex>w</tex> получится путь, оканчивающийся в одном из терминальных состояний.

Пусть <tex>A_{1}</tex> и <tex>A_{2}</tex> — [[Детерминированные конечные автоматы| детерминированные конечные автоматы]], задающие языки <tex>L_{1}</tex> и <tex>L_{2}</tex> над одним алфавитом <tex>\Sigma</tex>, соответственно. Совпадение языков ('''эквивалентность''' задающих их автоматов) означает, что любое слово, допустимое одним автоматом, допускается и другим. Назовём состояния <tex>p_{1}</tex> из <tex>A_{1}</tex> и <tex>p_{2}</tex> из <tex>A_{2}</tex> '''различимыми''', если существует строка <tex>w</tex> из символов <tex>\Sigma</tex>, для которой выполняется

Пусть <tex>eq(v, u, v)</tex> — функция, принимающая пару состояний из первого и второго автоматов и возвращающая некоторое значение булевского типа. Второй шаг алгоритма — установка <tex>eq(v, u, v)</tex> в <tex>false</tex> для всех пар <tex>\langle v, u, v \rangle</tex>, кроме <tex>\langle s_{1}, s_{2} \rangle</tex>. Также создаётся очередь, в которую помещается пара <tex>\langle s_{1}, s_{2} \rangle</tex>.

Третий шаг алгоритма — [[Обход в ширину|обход в ширину]]. Пусть на текущем шаге из очереди получена пара <tex>\langle u v \in A_{1}, v u \in A_{2} \rangle</tex>. Тогда для всех символов <tex>c \in \Sigma</tex> рассматриваются пары <tex>\langle uv', vu' \rangle : \delta_{1} (uv, c) = uv', \delta_{2} (vu, c) = vu'</tex>. Если <tex>eq(uv', vu')</tex> возвращает <tex>false</tex>, данное значение устанавливается в <tex>true</tex>, а в очередь добавляется пара <tex>\langle uv', vu' \rangle</tex>.

Автоматы <tex>A_{1}</tex> и <tex>A_{2}</tex> эквивалентны тогда и только тогда, когда после окончания работы алгоритма не существует такой пары <tex>\langle v, u, v \rangle</tex>, что <tex>eq(v, u, v)</tex> возвращает <tex>true</tex> и ровно одно из <tex>\langle v, u, v \rangle</tex> допускающее.

Пусть такой пары не существует. Возьмём произвольное слово <tex>w</tex> длины <tex>n</tex> и выпишем последовательность пар состояний <tex>\langle u_v_{i}, v_u_{i} \rangle</tex>: <tex>u_v_{0} = s_{1}, v_u_{0} = s_{2}</tex> и <tex>\forall i = 1 .. n</tex> справедливо <tex>\delta_{1} (u_v_{i-1}, w[i-1]) = u_v_{i}, \delta_{2} (v_u_{i-1}, w[i-1]) = v_u_{i}</tex>. Так как пара <tex>\langle u_v_{0}, v_u_{0} \rangle</tex> была в очереди, каждая из последующих пар в процессе алгоритма также побывала в очереди, значит, <tex>eq</tex> для них возвращает <tex>true</tex>. По предположению, или оба состояния <tex>\langle u_v_{n}, v_u_{n} \rangle</tex> допускающие в своих автоматах, или оба недопускающие. Таким образом, строка <tex>w</tex> или входит в оба языка, или не входит ни в один.

Пусть такая пара <tex>\langle v, u, v \rangle</tex> существует. Для определённости скажем, что <tex>u v \in A_{1}</tex> — допускающее. Рассмотрим строку <tex>w</tex>, состоящую из символов, в результате переходов по которым из <tex>\langle s_{1}, s_{2} \rangle</tex> в процессе обхода в ширину <tex>eq(v, u, v)</tex> было установлено в <tex>true</tex>. Строка <tex>w</tex> допускается первым автоматом, но не допускается вторым, значит, автоматы не эквивалентны.

Автомат [[Детерминированные конечные автоматы|Детерминированный конечный автомат]] <tex>A_{1}</tex> задаёт конечный язык тогда и только тогда, когда в <tex>A_{1}</tex> не существует состояния <tex>v</tex>, для которого выполняются три условия: