Изменения

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

|definition = [[Основные определения, связанные со строками#string|Слово ]] <tex>z \in \Sigma^*</tex> '''различает''' (англ. ''distinguish'') два состояния <tex>q_i</tex> и <tex>q_j</tex>, если * <tex> \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 ) </tex>.

|definition = Два <em> состояния</em> <tex>q_i</tex> и <tex>q_j</tex> называются '''эквивалентными''' <tex>(q_i \sim q_j)</tex>, если не существует [[Основные определения, связанные со строками#string|строки]], которая их различает, то есть <tex>\forall z \in \Sigma^*</tex> верно, что* <tex> \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 ) </tex>.

Заметим, что эквивалентность состояний действительно является [[Отношение эквивалентности|отношением эквивалентности]]. Так как <tex> \Leftrightarrow </tex> (равносильность) является отношением эквивалентности, и <tex> \forall z \in \Sigma^*\ \forall q \in Q \ \exists ! t : \langle q, z \rangle \vdash^* \langle tв детерминированном автомате всегда существует путь по любому слову, \varepsilon \rangle </tex>, что и доказывает, что описанное нами отношение является отношением эквивалентности. == Пример ==[[Файл:avtomat2.png|350px]] [[Файл:avtomat3.png|350px]] Эти два автомата принимают слова из языка слов длины не меньше одного, состоящих из символов алфавита <tex> \lbrace 0, 1\rbrace </tex>. Все допускающие состояния автоматов эквивалентны между собой.

== Алгоритм проверки эквивалентности автоматов =====Постановка задачиПример ===Даны два детерминированных конечных автомата <tex> \mathcal{A}_1 = \langle Q_1,\Sigma,\delta_1,s_{1}, T_1\subseteq Q_1 \rangle </tex> и <tex>\mathcal{A}_2 = \langle Q_2,\Sigma,\delta_2,s_{2}, T_2\subseteq Q_2 \rangle </tex>[[Файл:avtomat2. Требуется определить, эквивалентны ли ониpng|200px]] [[Файл:avtomat3.png|200px]]===Алгоритм===Рассмотрим такие семейства множеств:* Эти два автомата принимают слова из языка слов длины не меньше одного, состоящих из символов алфавита <tex> D_i = \lbrace \langle q0, p1\rangle | q \in Q_1, p \in Q_2, \exists w : |w| \le i, w </tex> различает <tex> q rbrace </tex> . Стартовые и <tex> p \rbrace </tex>;* <tex> E_i = D_i \setminus D_{i - 1} </tex>все допускающие состояния автоматов эквивалентны между собой.

Для <tex> D_i </tex> существует рекуррентная формула[[Категория:Теория формальных языков]]* <tex> D_i = D_{i - 1} \cup \lbrace \langle p, q \rangle | \exists c \in \Sigma [[Категория: \langle \delta(p, c), \delta(q, c) \rangle \in E_{i - 1} \rbrace </tex>.То есть <tex> D_i </tex> {{---}} объединение множества всех пар состояний, которые различаются строками длины меньшей <tex> i </tex> с множеством всех пар состояний, которые различаются строками длины ровно <tex>i</tex>.Автоматы и регулярные языки]]

Заметим, что <tex> \exists k == Проверка ДКА на эквивалентность ==Заданы два автомата: E_k = \varnothing </tex>, причем <tex> k \le |Q| ^ 2</tex>. Также заметим, что <tex> E_k = \varnothing \Rightarrow E_mathcal{k + 1A} = \varnothing _1 </tex>, так как в со стартовым состоянием <tex> D_{k+1}s_1 </tex> новых элементов не добавится, поэтому и <tex> D_\mathcal{k+1A} = D_k _2 </tex>.Значит:* со стартовым состоянием <tex> E_k = \varnothing \Rightarrow D_k = \lbrace \langle q, p\rangle | q \in Q_1, p \in Q_2, \exists w : w </tex> различает <tex> q </tex> и <tex> p \rbrace = \lbrace \langle q, p\rangle | (q \nsim p)\rbraces_2 </tex>соответственно. Нужно проверить их на эквивалентность.

Осталось найти такое '''Замечание:''' для реализации оба автомата обязательно должны иметь [[Детерминированные_конечные_автоматы#допускает|дьявольские состояния]].=== Проверка через минимизацию ===Для этого построим автомат <tex> k \mathcal{A} </tex> , содержащий все состояния обоих автоматов и изначальные переходы между ними. Стартовым состоянием в новом автомате можно сделать <tex> D_k s_1 </tex>, что или <tex> E_k = \varnothing s_2 </tex> тогда мы узнаем пары неэквивалентных состояний— это не имеет значения. При этом состояния одного из автоматов станут недостижимыми из новой стартовой вершины в новом автомате, останется только но для алгоритма это и не важно.<br>[[Файл:auto_equiq.png|470px]]<br>Осталось лишь проверить, что на эквивалентность состояния <tex> \langle s_1, </tex> и <tex> s_2 </tex> в полученном автомате. Их эквивалентность совпадает с эквивалентностью автоматов <tex> \rangle mathcal{A}_1 </tex> и <tex> \notin D_k mathcal{A}_2 </tex>. Для этого можно применить [[Минимизация_ДКА,_алгоритм_за_O(n%5E2)_с_построением_пар_различимых_состояний|алгоритм минимизации ДКА]], тогда который разбивает все состояния на классы эквивалентности. Если состояния <tex>s_1</tex> и <tex>s_2</tex> нового автомата в одном классе эквивалентности {{---}} исходные автоматы будут эквивалентны.

Будем строить <tex> D_i </tex> в порядке увеличения <tex> i </tex>, пока <tex> D_i \neq D_{i - 1}</tex>.Заметим, что <tex> D_0 = \lbrace \langle p, q\rangle | p \in T_1 \Leftrightarrow q \notin T_2 \rbrace </tex>, так как строка длины 0 одна {{---}} это <tex> \varepsilon </tex>, а <tex> \varepsilon </tex> различает только пары состоящие из одного терминального состояния Также можно минимизировать каждый автомат отдельно и одного нетерминальногопроверить минимизированные версии на изоморфизм.

Дальше будем получать <tex> D_i </tex> по рекуррентной формуле=== Проверка через BFS ===Два автомата можно также проверить на эквивалентность, пока используя [[Обход в ширину | обход в ширину]]. Будем синхронно обходить два автомата, начиная со стартовых состояний, в поисках такой строки, которая различает два состояния этих автоматов. То есть она будет допускаться одним автоматом, но не выполнится условие остановкибудет принадлежать языку другого.

Это можно реализовать проще: будем хранить для каждого состоянияПоскольку эквивалентные автоматы допускают один и тот же язык, из какого состояния есть переход при переходе по символу <tex> c </tex> одним и тем же символам в нашеобоих автоматах, слово должно приниматься обоими автоматами одновременно. В очередь будем класть пары неэквивалентных состояний. Дальше вытаскивая из очереди паруТо есть вершины, в которые мы перешли, должны быть либо одновременно терминальными, рассмотрим все пары состоянийлибо одновременно нетерминальными, из которых есть переход по одинаковому символу в элементы пары из очереди. Пометим их неэквивалентными что и положим в очередьпроверяет приведённый алгоритм. ====Псевдокод==== <font size color= 3green> <tex> q = // $\varnothing </tex> fill(neqmathtt{aut}[i][c]$ {{---}} номер состояния, false) for <tex> p_1 \in Q_1 в которое есть переход из состояния $i$ по символу $c$</texfont> for <tex> p_2 '''boolean''' $\in Q_2 </tex> if <tex> mathtt{bfsEquivalenceCheck}$(p_1 $\in T_1) mathtt{aut1}$ : '''int[][]''', $\neq (p_2 \in T_2mathtt{aut2}$ : '''int[][]''') </tex>: q $Q.\mathtt{push}(\langle s_1, s_2 \rangle) $ <texfont color=green>p_1</tex>,<tex> p_2</tex>) neq[<tex>p_1Q </tex>, <tex>p_2{{---}} очередь из пар состояний</texfont>] = True '''while not isEmpty(q)''' $Q \ne \varnothing $ <tex> \langle p_1 $u, p_2 v \rangle </tex> = qleftarrow Q.\mathtt{pop}()$ '''if''' $\mathtt{isTerminal1[u]} \ne \mathtt{isTerminal2[v]}$ '''return''' ''false'' $\mathtt{used[u][v]} \leftarrow $ ''true'' '''for <tex> ''' $c \in \Sigma </tex>$ '''if''' '''not''' $\mathtt{used[aut1[u][c]][aut2[v][c]]}$ for <tex> $Q.\deltamathtt{push}(e_1\langle \mathtt{aut1}[u][c], \mathtt{aut2}[v][c] \rangle) = p_1 </tex>$ '''return''' ''true''  for <tex> \deltaКорректность алгоритма следует из строго доказательства того факта, что если два состояния $u$ и $v$ различаются какой-то строкой, то они различаются строкой длины $O(e_2, cn) = p_2 </tex>$.  qИнтуитивное понимание алгоритма такое: пусть по строке $w$ мы пришли в состояния $ \langle u, v \rangle $, и пусть они оба нетерминальные.push(<tex>e_1</tex>После этого совершим переход по символу $c$ в состояния $ \langle u', <tex>e_2</tex>)v' \rangle $.   neqТогда если $\mathtt{isTerminal1[<tex>e_1</tex>u']} \ne \mathtt{isTerminal2[v']}$, <tex>e_2</tex>] то строка $wc$ различает эти два состояния. А значит автоматы не эквивалентны. == См. также == True if neq* [[<tex>s_1</tex>Минимизация_ДКА, <tex>s_2</tex>_алгоритм_за_O(n%5E2)_с_построением_пар_различимых_состояний|Алгоритм минимизации ДКА]] print* [[Минимизация ДКА, алгоритм Хопкрофта ("Not equivalent"сложность O(n log n) else print("Equivalent")]]</font>===Время работы алгоритма=Источники информации ==Алгоритм будет работать за <tex> O(|Q_1||Q_2||\Sigma|^2)<* [http://tex>stackoverflow.[[Категория: Теория формальных языков]com/questions/6905043/equivalence-between-two-automata/12623361#12623361 StackOverflow {{---}} Equivalence between two automata]