Эквивалентность состояний ДКА — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Проверка через BFS)
м (rollbackEdits.php mass rollback)
 
(не показано 16 промежуточных версий 7 участников)
Строка 1: Строка 1:
== Основные определения ==
+
== Связь эквивалентности состояний и различимости состояний ==
  
 
{{Определение
 
{{Определение
Строка 35: Строка 35:
 
== Проверка ДКА на эквивалентность ==
 
== Проверка ДКА на эквивалентность ==
 
Заданы два автомата: <tex> \mathcal{A}_1 </tex> со стартовым состоянием <tex> s_1 </tex> и <tex> \mathcal{A}_2 </tex> со стартовым состоянием <tex> s_2 </tex> соответственно. Нужно проверить их на эквивалентность.
 
Заданы два автомата: <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>
+
Для этого построим автомат <tex> \mathcal{A} </tex>, содержащий все состояния обоих автоматов и изначальные переходы между ними. Стартовым состоянием в новом автомате можно сделать <tex> s_1 </tex> или <tex> s_2 </tex> — это не имеет значения. При этом состояния одного из автоматов станут недостижимыми из новой стартовой вершины в новом автомате, но для алгоритма это и не важно.<br>
 
[[Файл:auto_equiq.png|470px]]<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> нового автомата в одном классе эквивалентности {{---}} исходные автоматы эквивалентны.
 
Осталось лишь проверить на эквивалентность состояния <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 ===
Алгоритм заключается в синхронном обходе автоматов в ширину, проверяя, что по пути сохраняются терминальные состояния.
+
Два автомата можно также проверить на эквивалентность, используя [[Обход в ширину | обход в ширину]]. Будем синхронно обходить два автомата, начиная со стартовых состояний, в поисках такой строки, которая различает два состояния этих автоматов. То есть она будет допускаться одним автоматом, но не будет принадлежать языку другого.
Поскольку '''эквивалентные''' автоматы '''допускают''' один  тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно '''терминальными''', либо одновременно '''нетерминальными''', что и проверяет приведённый алгоритм.  
 
  
<wikitex>
+
Поскольку эквивалентные автоматы допускают один и тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, либо одновременно нетерминальными, что и проверяет приведённый алгоритм.
Псевдокод:
+
==== Псевдокод ====
  <font color=green>// <tex>Q</tex> {{---}} очередь из пар состояний</font>
+
  <font color=green>// $\mathtt{aut}[i][c]$ {{---}} номер состояния, в которое есть переход из состояния $i$ по символу $c$</font>
  ''boolean'' '''function''' $\mathtt{bfsEquivalenceCheck}$($aut1$, $aut2$)
+
  '''boolean''' $\mathtt{bfsEquivalenceCheck}$($\mathtt{aut1}$ : '''int[][]''', $\mathtt{aut2}$ : '''int[][]'''):
     $Q.push( \langle s_1, s_2 \rangle ) $
+
     $Q.\mathtt{push}(\langle s_1, s_2 \rangle) $ <font color=green>// <tex> Q </tex> {{---}} очередь из пар состояний</font>
    $\mathtt{used1[s_1]} \leftarrow $ ''true''
+
     '''while''' $Q \ne \varnothing $  
    $\mathtt{used2[s_2]} \leftarrow $ ''true''
+
         $u, v \leftarrow Q.\mathtt{pop}()$
     '''while''' $Q \ne \varnothing $
+
         '''if''' $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$
         $u \leftarrow Q.front.first$
 
        $v \leftarrow Q.front.second$
 
        $\mathtt{Q.pop()}$
 
         '''if'''( $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$ )
 
 
             '''return''' ''false''
 
             '''return''' ''false''
         '''for''' $i \in \Sigma$
+
        $\mathtt{used[u][v]} \leftarrow $ ''true''
             '''if'''( '''not''' $\mathtt{used1[aut1[u][i]]}$ ||  '''not''' $\mathtt{used2[aut2[v][i]]} $)
+
         '''for''' $c \in \Sigma$
                 $Q.push( \langle \mathtt{aut1[u][i]}, \mathtt{aut2[v][i]} \rangle )$
+
             '''if''' '''not''' $\mathtt{used[aut1[u][c]][aut2[v][c]]}$
                $\mathtt{used1[aut1[u][i]]} \leftarrow $ ''true''
+
                 $Q.\mathtt{push}(\langle \mathtt{aut1}[u][c], \mathtt{aut2}[v][c] \rangle)$
                $\mathtt{used2[aut2[v][i]]} \leftarrow $ ''true''
+
    '''return''' ''true''
    '''return''' true;
+
 
</wikitex>
+
Корректность алгоритма следует из строго доказательства того факта, что если два состояния $u$ и $v$ различаются какой-то строкой, то они различаются строкой длины $O(n)$.
  
Замечание: в данной реализации оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские состояния]].
+
Интуитивное понимание алгоритма такое: пусть по строке $w$ мы пришли в состояния  $ \langle u, v \rangle $, и пусть они оба нетерминальные. После этого совершим переход по символу $c$ в состояния $ \langle u', v' \rangle $.  
  
<wikitex>
+
Тогда если $\mathtt{isTerminal1[u']} \ne \mathtt{isTerminal2[v']}$, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны.
Доказательство корректности:
 
Пусть по строке $w$ мы пришли в состояния  $ \langle u, v \rangle $, и пусть они нетерминальные.
 
Пусть мы перешли по символу $c$ в состояние $ \langle u', v' \rangle $ ($u$ может быть равно $u'$ или $v'$ может быть равно $u'$, но не оба сразу).
 
Тогда если $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны.
 
</wikitex>
 
  
 
== См. также ==  
 
== См. также ==  
Строка 83: Строка 73:
  
 
== Источники информации ==
 
== Источники информации ==
* [http://stackoverflow.com/questions/6905043/equivalence-between-two-automata/12623361#12623361| equivalence between two automata]
+
* [http://stackoverflow.com/questions/6905043/equivalence-between-two-automata/12623361#12623361 StackOverflow {{---}} Equivalence between two automata]

Текущая версия на 19:33, 4 сентября 2022

Связь эквивалентности состояний и различимости состояний

Определение:
Два автомата [math] \mathcal{A}_1 = \langle Q_1,\Sigma,\delta_1,s_{1}, T_1\subseteq Q_1 \rangle [/math] и [math]\mathcal{A}_2 = \langle Q_2,\Sigma,\delta_2,s_{2}, T_2\subseteq Q_2 \rangle [/math] называются эквивалентными (англ. equivalent), если они распознают один и тот же язык над алфавитом [math]\Sigma[/math], то есть [math]\mathcal{L}(\mathcal{A}_1) = \mathcal{L}(\mathcal{A}_2)[/math].


Определение:
Слово [math]z \in \Sigma^*[/math] различает (англ. distinguish) два состояния [math]q_i[/math] и [math]q_j[/math], если
  • [math] \langle q_i, z \rangle \vdash^* \langle t_1, \varepsilon \rangle, \langle q_j, z \rangle \vdash^* \langle t_2, \varepsilon \rangle \Rightarrow (t_1 \notin T \Leftrightarrow t_2 \in T) [/math].


Определение:
Два состояния [math]q_i[/math] и [math]q_j[/math] называются эквивалентными [math](q_i \sim q_j)[/math], если не существует строки, которая их различает, то есть [math]\forall z \in \Sigma^*[/math] верно, что
  • [math] \langle q_i, z \rangle \vdash^* \langle t_1, \varepsilon \rangle, \langle q_j, z \rangle \vdash^* \langle t_2, \varepsilon \rangle \Rightarrow (t_1 \in T \Leftrightarrow t_2 \in T) [/math].


Заметим, что эквивалентность состояний действительно является отношением эквивалентности. Так как [math] \Leftrightarrow [/math] (равносильность) является отношением эквивалентности и в детерминированном автомате всегда существует путь по любому слову, описанное нами отношение является отношением эквивалентности.

Лемма:
[math] \mathcal{A} = \langle Q, \Sigma, \delta, s, T \rangle [/math], [math] p_1, p_2, q_1, q_2 \in Q [/math], [math] q_i = \delta(p_i, c) [/math], [math] w \in \Sigma^*[/math] различает [math] q_1 [/math] и [math] q_2 [/math]. Тогда [math]cw[/math] различает [math] p_1 [/math] и [math] p_2 [/math].
Доказательство:
[math]\triangleright[/math]

[math] \langle p_i, cw \rangle \vdash \langle q_i, w \rangle \vdash^* \langle t_i, \varepsilon \rangle [/math]

А значит, по условию различимости для [math] q_1 [/math] и [math] q_2[/math] , [math] t_1 \in T \Leftrightarrow t_2 \notin T [/math]
[math]\triangleleft[/math]

Пример

Avtomat2.png Avtomat3.png

Эти два автомата принимают слова из языка слов длины не меньше одного, состоящих из символов алфавита [math] \lbrace 0, 1\rbrace [/math]. Стартовые и все допускающие состояния автоматов эквивалентны между собой.

Проверка ДКА на эквивалентность

Заданы два автомата: [math] \mathcal{A}_1 [/math] со стартовым состоянием [math] s_1 [/math] и [math] \mathcal{A}_2 [/math] со стартовым состоянием [math] s_2 [/math] соответственно. Нужно проверить их на эквивалентность.

Замечание: для реализации оба автомата обязательно должны иметь дьявольские состояния.

Проверка через минимизацию

Для этого построим автомат [math] \mathcal{A} [/math], содержащий все состояния обоих автоматов и изначальные переходы между ними. Стартовым состоянием в новом автомате можно сделать [math] s_1 [/math] или [math] s_2 [/math] — это не имеет значения. При этом состояния одного из автоматов станут недостижимыми из новой стартовой вершины в новом автомате, но для алгоритма это и не важно.
Auto equiq.png
Осталось лишь проверить на эквивалентность состояния [math] s_1 [/math] и [math] s_2 [/math] в полученном автомате. Их эквивалентность совпадает с эквивалентностью автоматов [math] \mathcal{A}_1 [/math] и [math] \mathcal{A}_2 [/math]. Для этого можно применить алгоритм минимизации ДКА, который разбивает все состояния на классы эквивалентности. Если состояния [math]s_1[/math] и [math]s_2[/math] нового автомата в одном классе эквивалентности — исходные автоматы эквивалентны.

Также можно минимизировать каждый автомат отдельно и проверить минимизированные версии на изоморфизм.

Проверка через BFS

Два автомата можно также проверить на эквивалентность, используя обход в ширину. Будем синхронно обходить два автомата, начиная со стартовых состояний, в поисках такой строки, которая различает два состояния этих автоматов. То есть она будет допускаться одним автоматом, но не будет принадлежать языку другого.

Поскольку эквивалентные автоматы допускают один и тот же язык, при переходе по одним и тем же символам в обоих автоматах, слово должно приниматься обоими автоматами одновременно. То есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, либо одновременно нетерминальными, что и проверяет приведённый алгоритм.

Псевдокод

// $\mathtt{aut}[i][c]$ — номер состояния, в которое есть переход из состояния $i$ по символу $c$
boolean $\mathtt{bfsEquivalenceCheck}$($\mathtt{aut1}$ : int[][], $\mathtt{aut2}$ : int[][]):
    $Q.\mathtt{push}(\langle s_1, s_2 \rangle) $ // [math] Q [/math] — очередь из пар состояний
    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$ мы пришли в состояния $ \langle u, v \rangle $, и пусть они оба нетерминальные. После этого совершим переход по символу $c$ в состояния $ \langle u', v' \rangle $.

Тогда если $\mathtt{isTerminal1[u']} \ne \mathtt{isTerminal2[v']}$, то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны.

См. также

Источники информации