Изменения
→Псевдокод
== Основные определения Связь эквивалентности состояний и различимости состояний ==
{{Определение
== Проверка ДКА на эквивалентность ==
Заданы два автомата: <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>
[[Файл:auto_equiq.png|470px]]<br>
Осталось лишь проверить на эквивалентность состояния <tex> s_1 </tex> и <tex> s_2 </tex> в полученном автомате. Их эквивалентность совпадает с эквивалентностью автоматов <tex> \mathcal{A}_1 </tex> и <tex> \mathcal{A}_2 </tex>. Для этого можно применить [[Минимизация_ДКА,_алгоритм_за_O(n%5E2)_с_построением_пар_различимых_состояний|алгоритм минимизации ДКА]], который разбивает все состояния на классы эквивалентности. Если состояния <tex>s_1</tex> и <tex>s_2</tex> нового автомата в одном классе эквивалентности {{---}} исходные автоматы эквивалентны.
Также можно минимизировать каждый автомат отдельно и проверить минимизированные версии на изоморфизм.
=== Проверка через BFS ===
Поскольку эквивалентные автоматы допускают один и тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, либо одновременно нетерминальными, что и проверяет приведённый алгоритм.
==== Псевдокод ====
<wikitex>
'''return''' ''false''
$\mathtt{used[u][v]} \leftarrow $ ''true'' '''for''' $i c \in \Sigma$ '''if'''( '''not''' $\mathtt{used1used[aut1[u][ic]]}$ || '''not''' $\mathtt{used2[aut2[v][ic]]} $) '''insert''' $ Q.\mathtt{push}(\langle \mathtt{aut1}[u][ic]}, \mathtt{aut2}[v][ic]} \rangle )$ '''return''' ''true'' Корректность алгоритма следует из строго доказательства того факта, что если два состояния $u$ и $v$ различаются какой-то строкой, то они различаются строкой длины $O(n)$. Интуитивное понимание алгоритма такое: пусть по строке $w$ мы пришли в состояния $ \langle u, v \rangle $, и пусть они оба нетерминальные. После этого совершим переход по символу $c$ в состояния $ \langle u', v' \in Q rangle $. Тогда если $\mathtt{used1[aut1isTerminal1[u][i]']} \leftarrow $ ''true'' $ne \mathtt{used2[aut2isTerminal2[v][i]']} \leftarrow $ ''true'' '''return''' true;, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны.
</wikitex>
== См. также ==
== Источники информации ==
* [http://stackoverflow.com/questions/6905043/equivalence-between-two-automata/12623361#12623361| equivalence StackOverflow {{---}} Equivalence between two automata]
