Эквивалентность состояний ДКА — различия между версиями
(→Проверка через BFS) |
(→Псевдокод) |
||
Строка 53: | Строка 53: | ||
'''boolean''' $\mathtt{bfsEquivalenceCheck}$($\mathtt{aut1}$ : '''int[][]''', $\mathtt{aut2}$ : '''int[][]'''): | '''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> | $Q.\mathtt{push}(\langle s_1, s_2 \rangle) $ <font color=green>// <tex>Q</tex> {{---}} очередь из пар состояний</font> | ||
− | |||
− | |||
'''while''' $Q \ne \varnothing $ | '''while''' $Q \ne \varnothing $ | ||
$u, v \leftarrow Q.\mathtt{pop}()$ | $u, v \leftarrow Q.\mathtt{pop}()$ | ||
Строка 62: | Строка 60: | ||
'''if''' '''not''' $\mathtt{used1[aut1}[u][c]]$ '''or''' '''not''' $\mathtt{used2[aut2}[v][c]]$ | '''if''' '''not''' $\mathtt{used1[aut1}[u][c]]$ '''or''' '''not''' $\mathtt{used2[aut2}[v][c]]$ | ||
$Q.\mathtt{push}(\langle \mathtt{aut1}[u][c], \mathtt{aut2}[v][c] \rangle)$ | $Q.\mathtt{push}(\langle \mathtt{aut1}[u][c], \mathtt{aut2}[v][c] \rangle)$ | ||
− | + | $\mathtt{used1[aut1}[u][c]] \leftarrow $ ''true'' | |
− | + | $\mathtt{used2[aut2}[v][c]] \leftarrow $ ''true'' | |
'''return''' ''true'' | '''return''' ''true'' | ||
Версия 22:50, 8 июня 2016
Содержание
Связь эквивалентности состояний и различимости состояний
Определение: |
Два автомата | и называются эквивалентными (англ. equivalent), если они распознают один и тот же язык над алфавитом , то есть .
Определение: |
Слово различает (англ. distinguish) два состояния и , если
|
Определение: |
Два состояния строки, которая их различает, то есть верно, что
| и называются эквивалентными , если не существует
Заметим, что эквивалентность состояний действительно является отношением эквивалентности. Так как (равносильность) является отношением эквивалентности и в детерминированном автомате всегда существует путь по любому слову, описанное нами отношение является отношением эквивалентности.
Лемма: |
, , , различает и . Тогда различает и . |
Доказательство: |
А значит, по условию различимости для и , |
Пример
Эти два автомата принимают слова из языка слов длины не меньше одного, состоящих из символов алфавита
. Стартовые и все допускающие состояния автоматов эквивалентны между собой.Проверка ДКА на эквивалентность
Заданы два автомата:
со стартовым состоянием и со стартовым состоянием соответственно. Нужно проверить их на эквивалентность.Замечание: для реализации оба автомата обязательно должны иметь дьявольские состояния.
Проверка через минимизацию
Для этого построим автомат
Осталось лишь проверить на эквивалентность состояния и в полученном автомате. Их эквивалентность совпадает с эквивалентностью автоматов и . Для этого можно применить алгоритм минимизации ДКА, который разбивает все состояния на классы эквивалентности. Если состояния и нового автомата в одном классе эквивалентности — исходные автоматы эквивалентны.
Также можно минимизировать каждый автомат отдельно и проверить минимизированные версии на изоморфизм.
Проверка через BFS
Два автомата можно также проверить на эквивалентность, используя обход в ширину. Будем синхронно обходить два автомата, начиная со стартовых состояний, в поисках такой строки, которая различает два состояния этих автоматов. То есть она будет допускаться одним автоматом, но не будет принадлежать языку другого.
Поскольку эквивалентные автоматы допускают один и тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, либо одновременно нетерминальными, что и проверяет приведённый алгоритм.
Псевдокод
<wikitex>
// $\mathtt{aut}[i][c]$ — номер состояния, в которое есть переход из состояния $i$ по символу $c$
boolean $\mathtt{bfsEquivalenceCheck}$($\mathtt{aut1}$ : int[][], $\mathtt{aut2}$ : int[][]):
$Q.\mathtt{push}(\langle s_1, s_2 \rangle) $ //
— очередь из пар состояний
while $Q \ne \varnothing $
$u, v \leftarrow Q.\mathtt{pop}()$
if $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$
return false
for $c \in \Sigma$
if not $\mathtt{used1[aut1}[u][c]]$ or not $\mathtt{used2[aut2}[v][c]]$
$Q.\mathtt{push}(\langle \mathtt{aut1}[u][c], \mathtt{aut2}[v][c] \rangle)$
$\mathtt{used1[aut1}[u][c]] \leftarrow $ true
$\mathtt{used2[aut2}[v][c]] \leftarrow $ true
return true
Корректность алгоритма следует из строго доказательства того факта, что если два состояния $u$ и $v$ различаются какой-то строкой, то они различаются строкой длины $O(n)$.
Интуитивное понимание алгоритма такое: пусть по строке $w$ мы пришли в состояния $ \langle u, v \rangle $, и пусть они оба нетерминальные. После этого совершим переход по символу $c$ в состояния $ \langle u', v' \rangle $.
Тогда если $\mathtt{isTerminal1[u']} \ne \mathtt{isTerminal2[v']}$, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны. </wikitex>