Изменения

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

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

1206 байт добавлено, 19:33, 4 сентября 2022
м
rollbackEdits.php mass rollback
== Основные определения Связь эквивалентности состояний и различимости состояний ==
{{Определение
== Проверка ДКА на эквивалентность ==
Заданы два автомата: <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 ===Два автомата обязательно должны иметь можно также проверить на эквивалентность, используя [[Детерминированные_конечные_автоматы#допускаетОбход в ширину |дьявольские состоянияобход в ширину]]. Будем синхронно обходить два автомата, начиная со стартовых состояний, в поисках такой строки, которая различает два состояния этих автоматов. То есть она будет допускаться одним автоматом, но не будет принадлежать языку другого.
=== Проверка через 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> '''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{used[aut1[u][c]][aut2[v][c]]}$ $Q.\mathtt{push}(\langle \mathtt{aut1}[u][c], либо одновременно \mathtt{aut2}[v][c] \rangle)$ '''return''''нетерминальными'true'' Корректность алгоритма следует из строго доказательства того факта, что если два состояния $u$ и проверяет приведённый алгоритм$v$ различаются какой-то строкой, то они различаются строкой длины $O(n)$.
ПсевдокодИнтуитивное понимание алгоритма такое:пусть по строке $w$ мы пришли в состояния bfs_equivalence_check(aut1, aut2) '''insert''' <tex>$ \{s_1langle u, s_2\}</tex> in <tex>Q </tex> used1[0] <tex> \leftarrow </tex> true; used2[0] <tex> \leftarrow </tex> true; '''while''' <tex>Q \ne \varnothing </tex> u <tex> \leftarrow </tex> Q.front.first; v <tex> \leftarrow </tex> Q.frontrangle $, и пусть они оба нетерминальные.second; pop(Q); '''if'''(isTerminal1[u] != isTerminal2[v]) '''return''' false; '''for''' <tex>i После этого совершим переход по символу $c$ в состояния $ \in \Sigma</tex> '''if'''(!used1[aut1[langle u][i]] || !used2[aut2[v][i]]) '''insert''' <tex>\{</tex>aut1[u][i], aut2[v][i]<tex>' \}</tex> in <tex>Q</tex> used1[aut1[u][i]] <tex> \leftarrow </tex> true; used2[aut2[v][i]] <tex> \leftarrow </tex> true; '''return''' true;rangle $.
Замечание: в данной реализации оба автомата обязательно должны иметь Тогда если $\mathtt{isTerminal1[u']} \ne \mathtt{isTerminal2[Детерминированные_конечные_автоматы#допускает|дьявольские v']}$, то строка $wc$ различает эти два состояния]]. А значит автоматы не эквивалентны.
== См. также ==
* [[Минимизация_ДКА,_алгоритм_за_O(n%5E2)_с_построением_пар_различимых_состояний|алгоритм Алгоритм минимизации ДКА]]
* [[Минимизация ДКА, алгоритм Хопкрофта (сложность O(n log n))]]
 
== Источники информации ==
* [http://stackoverflow.com/questions/6905043/equivalence-between-two-automata/12623361#12623361| equivalence StackOverflow {{---}} Equivalence between two automata]
1632
правки

Навигация