Обобщенный автомат Бюхи - Generalized Büchi automaton

В теория автоматов, обобщенный автомат Бюхи это вариант Büchi автомат. Отличие от автомата Бюхи состоит в том, что он принимает условие, то есть набор наборов состояний. Запуск принимается автоматом, если он бесконечно часто посещает хотя бы одно состояние из каждого набора условий приема. Обобщенные автоматы Бюхи эквивалентны по выразительной способности автоматам Бюхи; преобразование дано здесь.

В формальная проверка, то проверка модели метод должен получить автомат из LTL формула, определяющая свойство программы. Есть алгоритмы что переводит LTL формула обобщенного автомата Бюхи.^[1][2][3][4]для этого. Понятие обобщенного автомата Бюхи было введено специально для этого перевода.

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

Формально обобщенный автомат Бюхи - это набор А = (Q, Σ, Δ,Q₀,${\displaystyle {\cal {F}}}$), который состоит из следующих компонентов:

• Q это конечный набор. Элементы Q называются состояния из А.
• Σ - конечное множество, называемое алфавит из А.
• Δ:Q × Σ →2^Q это функция, называемая переходное отношение из А.
• Q₀ это подмножество Q, называемые начальными состояниями.
• ${\displaystyle {\cal {F}}}$ это условие приема, который состоит из нуля или более принимающих наборов. Каждый принимающий набор ${\displaystyle F_{i}\in {\cal {F}}}$ это подмножество Q.

А принимает именно те прогоны, в которых набор бесконечно часто встречающихся состояний содержит по крайней мере состояние из каждого принимающего набора ${\displaystyle F_{i}\in {\cal {F}}}$. Обратите внимание, что может быть нет принимающие множества, и в этом случае любой бесконечный цикл тривиально удовлетворяет этому свойству.

Для более полного формализма см. Также ω-автомат.

Обозначенный обобщенный автомат Бюхи

Обобщенный автомат Бюхи с метками - это еще один вариант, в котором входные данные связаны как метки с состояниями, а не с переходами. Он был введен Gerth et al.^[3]

Формально помеченный обобщенный автомат Бюхи - это набор А = (Q, Σ, L, Δ,Q₀,${\displaystyle {\cal {F}}}$), который состоит из следующих компонентов:

• Q это конечный набор. Элементы Q называются состояния из А.
• Σ конечное множество, называемое алфавит из А.
• L: Q → 2^Σ это функция, называемая функция маркировки из А.
• Δ:Q → 2^Q это функция, называемая переходное отношение из А.
• Q₀ это подмножество Q, называемые начальными состояниями.
• ${\displaystyle {\cal {F}}}$ это условие приема, который состоит из нуля или более принимающих наборов. Каждый принимающий набор ${\displaystyle F_{i}\in {\cal {F}}}$ это подмножество Q.

Позволять ш = а₁а₂ ... быть ω-слово над алфавитом Σ. р₁,р₂, ... это пробег А на слово ш если р₁  ∈  Q₀ и для каждого я ≥ 0,р_{я + 1} ∈ Δ (р_я) и а_я ∈ L(р_я).А принимает именно те прогоны, в которых набор бесконечно часто встречающихся состояний содержит по крайней мере состояние из каждого принимающего набора ${\displaystyle F_{i}\in {\cal {F}}}$. Обратите внимание, что может быть нет принимающие множества, и в этом случае любой бесконечный цикл тривиально удовлетворяет этому свойству.

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

Рекомендации

1. МОЙ. Варди и П. Вольпер, Рассуждения о бесконечных вычислениях, Информация и вычисления, 115 (1994), 1–37.
2. Ю. Кестен, З. Манна, Х. Макгуайр, А. Пнуели, Алгоритм принятия решений для полной временной логики высказываний, CAV’93, Элунда, Греция, LNCS 697, Springer – Verlag, 97-109.
3. Р. Герт, Д. Пелед, М.Ю. Варди и П. Вольпер, "Простая автоматическая проверка линейной темпоральной логики на лету", Proc. IFIP / WG6.1 Symp. Спецификация протокола, тестирование и проверка (PSTV95), стр. 3-18, Варшава, Польша, Chapman & Hall, июнь 1995 г.
4. П. Гастин и Д. Одду, Быстрый перевод LTL в автомат Бюхи, Тринадцатая конференция по компьютерной проверке (CAV '01), номер 2102 в LNCS, Springer-Verlag (2001), стр. 53–65.