1632
правки
Изменения
м
<wikitex>
$\mathtt{used1[aut1}[u][c]] \leftarrow $ ''true''
$\mathtt{used2[aut2}[v][c]] \leftarrow $ ''true''
</wikitex>
rollbackEdits.php mass rollback
'''Замечание:''' для реализации оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские состояния]].
=== Проверка через минимизацию ===
Для этого построим автомат <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 ===
Два автомата можно также проверить на эквивалентность, используя [[Обход в ширину | обход в ширину]]. Будем синхронно обходить два автомата, начиная со стартовых состояний, в поисках такой строки, которая различает два состояний состояния этих автоматов. То есть она будет допускаться одним автоматом, но не будет принадлежать языку другого.
Поскольку эквивалентные автоматы допускают один и тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, либо одновременно нетерминальными, что и проверяет приведённый алгоритм.
==== Псевдокод ====
<font color=green>// $\mathtt{aut}[i][c]$ {{---}} номер состояния, в которое есть переход из состояния $i$ по символу $c$</font>
'''boolean''' $\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, v \leftarrow Q.\mathtt{pop}()$
'''if''' $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$
'''return''' ''false''
$\mathtt{used[u][v]} \leftarrow $ ''true''
'''for''' $c \in \Sigma$
'''if''' '''not''' $\mathtt{used1used[aut1}[u][c]]$ '''or''' '''not''' $\mathtt{used2[aut2}[v][c]]}$
$Q.\mathtt{push}(\langle \mathtt{aut1}[u][c], \mathtt{aut2}[v][c] \rangle)$
'''return''' ''true''
Тогда если $\mathtt{isTerminal1[u']} \ne \mathtt{isTerminal2[v']}$, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны.
== См. также ==
== Источники информации ==
* [http://stackoverflow.com/questions/6905043/equivalence-between-two-automata/12623361#12623361| equivalence StackOverflow {{---}} Equivalence between two automata]
