Изменения

Перейти к: навигация, поиск

Эквивалентность состояний ДКА

391 байт добавлено, 22:58, 8 июня 2016
→‎Псевдокод
== Проверка ДКА на эквивалентность ==
Заданы два автомата: <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>
Псевдокод: <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 ) $ $\mathtt<font color=green>// <tex>Q</tex> {{used1[s_1]---} \leftarrow $ ''true'' $\mathtt{used2[s_2]} \leftarrow $ ''true''очередь из пар состояний</font> '''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''
$\mathtt{used1[u]} \leftarrow $ ''true'' $\mathtt{used2[v]} \leftarrow $ ''true'' '''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][i]]} \leftarrow $ '''return'true'' $\mathtt{used2[aut2[v][i]]} \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>
== Источники информации ==
* [http://stackoverflow.com/questions/6905043/equivalence-between-two-automata/12623361#12623361| equivalence StackOverflow {{---}} Equivalence between two automata]
Анонимный участник
Источник — «http://neerc.ifmo.ru/wiki/index.php?title=Служебная:Сравнение_версий/40440...55011»

Навигация