Полудетерминированный автомат Бюхи - Semi-deterministic Büchi automaton

В теория автоматов, а полудетерминированный автомат Бюхи (также известен как Автомат Бюхи детерминированный в пределе,^[1] или же предельно-детерминированный автомат Бюхи^[2]) - особый тип Büchi автомат. В таком автомате множество состояний может быть разделенный на два подмножества: одно подмножество образует детерминированный автомат, а также содержит все принимающие состояния.

Для каждого автомата Бюхи полудетерминированный автомат Бюхи может быть построен так что оба признают одно и то же ω-язык. Но детерминированный автомат Бюхи может не существовать для того же ω-языка.

Мотивация

При стандартной проверке модели на соответствие свойствам линейной временной логики (LTL) достаточно перевести формулу LTL в недетерминированный автомат Бюхи. Но при проверке вероятностной модели формулы LTL обычно переводятся в детерминированные автоматы Рабина (DRA), как, например, в инструменте PRISM. Однако не нужен полный детерминированный автомат. В самом деле, полудетерминированных автоматов Бюхи достаточно для проверки вероятностных моделей.

Формальное определение

А Büchi автомат (Q, Σ, ∆, Q₀, F) называется полудетерминированным, если Q - это объединение двух непересекающихся подмножеств N и D таких, что F ⊆ D и для любого d ∈ D автомат (D, Σ, ∆, {d}, F) детерминирован.

Преобразование из автомата Бюхи

Любой данный автомат Бюхи можно преобразовать в полудетерминированный автомат Бюхи, который распознает тот же язык, используя следующие строительство.

Предполагать А= (Q, Σ, ∆, Q₀, F) - автомат Бюхи. Позволять Pr - функция проекции, которая принимает набор состояний S и символ а ∈ Σ и возвращает множество состояний {q '| ∃q ∈ S и (q, a, q ') ∈ ∆}. Эквивалентный полудетерминированный автомат Бюхи: А '= (N ∪ D, Σ, ∆ ', Q'₀, F '), где

N = 2^Q и D = 2^Q×2^Q
Q '₀ = {Q₀}
∆' = ∆₁ ∪ ∆₂ ∪ ∆₃ ∪ ∆₄
- ∆₁ = {(S, a, S ') | S '=Pr(S, а)}
- ∆₂ = {(S, a, ({q '}, ∅)) | ∃q ∈ S и (q, a, q ') ∈ ∆}
- ∆₃ = {((L, R), a, (L ', R')) | L ≠ R и L '=Pr(L, a) и R '= (L'∩F) ∪Pr(R, a)}
- ∆₄ = {((L, L), a, (L ', R')) | L '=Pr(L, a) и R '= (L'∩F)}
F '= {(L, L) | L ≠ ∅}

Обратите внимание на структуру состояний и переходов A ′. Государства A ′ делятся на N и D. N-состояние определяется как элемент набор мощности государств А. D-состояние определяется как пара элементов мощности множества состояний А. Отношение перехода А ' представляет собой объединение четырех частей: ∆₁, ∆₂, ∆₃, и ∆₄. ∆₁-только переходы принимают А ' из N-состояния в N-состояние. Только ∆₂-переходы могут принимать А ' из N-состояния в D-состояние. Отметим, что только ∆₂-переходы могут вызвать недетерминизм в А ' . ∆₃ и ∆₄-переходы принимают А ' из D-состояния в D-состояние. По конструкции, А ' является полудетерминированным автоматом Бюхи. Доказательство L (A ') = L (A) следует.

Для ω-слова ш= а₁, а₂,... , позволять ш(i, j) - конечный отрезок a_{я + 1}, ..., а_j-1, а_j из ш.

L (А ') ⊆ L (А)

Доказательство: Позволять ш ∈ L (A '). Исходное состояние А ' является N-состоянием, а все принимающие состояния в F 'являются D-состояниями. Следовательно, любой приемный запуск А ' должен следовать за ∆₁ для конечного числа переходов в начале, затем возьмем переход в ∆₂ перейти в D-состояния, а затем взять ∆₃ и ∆₄ переходы навсегда. Пусть ρ '= S₀, ..., S_п-1, (L₀,Р₀), (L₁,Р₁), ... быть таким согласным А ' на ш.

По определению ∆₂, L₀ должен быть одноэлементным набором. Пусть L₀ = {s}. В силу определений ∆₁ и ∆₂существует префикс запуска s₀, ..., с_п-1, с из А на слове w (0, n) такое, что s_j ∈ S_j. Поскольку ρ '- приемный ряд А ' , некоторые состояния в F 'посещаются бесконечно часто. Следовательно, существует строго возрастающая и бесконечная последовательность индексов i₀,я₁, ... такие, что я₀= 0 и для каждого j> 0 L_{я_j}= R_{я_j} и я_{я_j}≠ ∅. Для всех j> 0 положим m = i_j-я_j-1. В силу определений ∆₃ и ∆₄, для каждого q_м ∈ L_{я_j}, существует состояние q₀ ∈ L_{я_j-1} и пробег q₀, ..., q_м из А на словном сегменте ш(п + я_j-1, п + я_j) такое, что для некоторого 0 k ∈ F. Мы можем организовать собранные таким образом отрезки цикла с помощью следующих определений.

Позволять предшественник(q_м, j) = q₀.
Позволять пробег(s, 0) = s₀, ..., с_п-1, s и при j> 0 пробег(q_м, j) = q₁, ..., q_м

Теперь приведенные выше сегменты цикла будут объединены, чтобы выполнить бесконечный приемный цикл А. Рассмотрим дерево, множество узлов которого ∪_j≥0 L_{я_j} × {j}. Корень равен (s, 0), а родительский элемент узла (q, j) равен (предшественник(q, j), j-1) Это бесконечное, конечно ветвящееся и полносвязное дерево. Следовательно, по Лемма Кёнига, существует бесконечный путь (q₀, 0), (q₁, 1), (q₂, 2), ... в дереве. Таким образом, ниже приводится приемный запуск А

пробег(q₀,0)⋅пробег(q₁,1)⋅пробег(q₂,2)⋅...

Следовательно, ш принимается А.

L (А) ⊆ L (А ')

Доказательство: Определение функции проекции Pr может быть расширен таким образом, что во втором аргументе он может принимать конечное слово. Пусть для некоторого набора состояний S, конечного слова w и символа a Pr(S, aw) =Pr(Pr(S, a), w) и Pr(S, ε) = S. Пусть ш ∈ L (A) и ρ = q₀, q₁, ... быть приемлемым пробегом А на ш. Сначала докажем следующую полезную лемму.

Лемма 1.: Существует такой индекс n, что q_п ∈ F и для любого m ≥ n существует k> m такое, что Pr ({q_п }, w (n, k)) = Pr ({q_м }, w (m, k)).; Доказательство: Pr ({q_п }, w (n, k)) ⊇ Pr ({q_м }, w (m, k)) выполняется, поскольку существует путь из q_п к q_м. Докажем обратное от противного. Предположим, что для всех n существует m ≥ n такое, что для всех k> m Pr ({q_п }, w (n, k)) ⊃ Pr ({q_м }, w (m, k)) выполняется. Предположим, что p - количество состояний в А. Следовательно, существует строго возрастающая последовательность индексов n₀, п₁, ..., п_п такое, что для всех k> n_п, Pr ({q_{п_я} }, w (n_я, k)) ⊃ Pr ({q_{п_{я + 1}} }, w (n_{я + 1}, л)). Следовательно, Pr ({q_{п_п} }, w (n_п, к)) = ∅. Противоречие.

В любом беге, А ' может только один раз сделать недетерминированный выбор, то есть когда он выбирает Δ₂ переход и остальная часть исполнения А ' детерминирован. Пусть n таково, что удовлетворяет лемме 1. Сделаем А ' взять Δ₂ переход на n-м шаге. Итак, определим серию ρ '= S₀, ..., S_п-1, ({q_п}, ∅), (L₁,Р₁), (L₂,Р₂),... из А ' на слово ш. Покажем, что ρ '- приемный пробег. L_я ≠ ∅ потому что существует бесконечный пробег А проходя через q_п. Итак, нам осталось показать, что L_я= R_я происходит бесконечно часто. Предположим противное, тогда существует такой индекс m, что для всех i ≥ m L_я≠ R_я. Пусть j> m такое, что q_{j + n} ∈ F, поэтому q_{j + n} ∈ R_j. По лемме 1 существуют k> j такие, что L_k = Pr ({q_п }, w (n, k + n)) = Pr ({q_{j + n} }, w (j + n, k + n)) ⊆ R_k. Итак, L_k= R_kПолучено противоречие. Следовательно, ρ '- приемный пробег и ш ∈ L (A ').