Омега-регулярный язык - Omega-regular language

В ω-регулярные языки являются классом ω-языки которые обобщают определение обычные языки до бесконечных слов. Бючи в 1962 году показал, что ω-регулярные языки - это в точности те, которые определимы в определенной монадической логика второго порядка называется S1S.

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

Ω-язык L ω-регулярен, если имеет вид

А^ω где А это непустой обычный язык, не содержащий пустой строки
AB, конкатенация регулярного языка А и ω-регулярный язык B (Обратите внимание, что BA является не четко определенный)
А ∪ B где А и B являются ω-регулярными языками (это правило может применяться только конечное число раз)

Элементы А^ω получаются путем объединения слов из А бесконечно много раз. Обратите внимание, что если А регулярно, А^ω не обязательно ω-регулярный, так как А может быть {ε}, множество, содержащее только пустой строки, в таком случае А^ω=А, который не является ω-языком и, следовательно, не является ω-регулярным языком.

Эквивалентность автомату Бюхи

Теорема: Ω-язык распознается Büchi автомат тогда и только тогда, когда это ω-регулярный язык.

Доказательство: Каждый ω-регулярный язык распознается недетерминированным Büchi автомат; перевод конструктивный. С использованием закрывающие свойства автоматов Бюхи и структурной индукции по определению ω-регулярного языка, легко показать, что автомат Бюхи может быть построен для любого данного ω-регулярного языка.

И наоборот, для данного автомата Бюхи А = (Q, Σ, Δ, я, F), мы построим ω-регулярный язык, а затем покажем, что этот язык распознается А. Для ω-слова ш = а₁а₂... позволять ш(я,j) - конечный отрезок а_я+1...а_j-1а_j из ш.Для каждого q, q ' ∈ Q, определим обычный язык L_{q, q '} принимается конечным автоматом (Q, Σ, Δ, q, {q '}).

Лемма: Мы утверждаем, что автомат Бюхи А распознает язык ⋃_{q∈я, q'∈F} L_{q, q '} (L_{д ', д'} - {ε})^ω.

Доказательство: Предположим слово ш ∈ L (А) и q₀, q₁, q₂, ... это приемный запуск А на ш. Следовательно, q₀ в я и должно быть состояние q 'в F такое, что q 'встречается бесконечно часто в принимающем прогоне. Выберем возрастающую бесконечную последовательность индексов i₀,я₁,я₂... такие, что для всех k≥0 q_{я_k} это q '. Следовательно, ш(0, я₀)∈L_{q₀, q '} и для всех k≥0 ш(я_k,я_{к + 1})∈L_{д ', д'} . Следовательно, ш ∈ L_{q₀, q '} (L_{д ', д'} )^ω.

Теперь предположим ш ∈ L_{q, q '} (L_{д ', д'} - {ε})^ω для некоторого q∈я и q'∈F. Следовательно, существует бесконечная и строго возрастающая последовательность i₀,я₁,я₂... такой, что ш(0, я₀) ∈ L_{q, q '} и для всех k≥0ш(я_k,я_{к + 1})∈L_{д ', д'} . По определению L_{q, q '}, существует конечный пробег A от q до q 'на слове ш(0, я₀). Для всех k≥0 существует конечный пробег A от q 'до q' на слове ш(я_k,я_{к + 1}). По этой конструкции существует серия А, которая начинается с q и в которой q 'встречается бесконечно часто. Следовательно, ш ∈ L (А).

Список используемой литературы

В. Томас, «Автоматы на бесконечных объектах». В Ян ван Леувен, редактор, Справочник по теоретической информатике, том B: Формальные модели и семантика, страницы 133-192. Издательство Elsevier Science Publishers, Амстердам, 1990 г.