Автомат Бюхи

Пусть AP- множество атомарных предложений. Автоматом Бюхи[1, 4]над алфавитом 2^apназывается четверка A = (Q, q₀, δ, F),в которой

• Q - конечное множество состояний;

• q₀- начальное состояние;

• тотальное отношение переходов;

• - множество допускающих состояний.

Автомат Бюхи A допускает слово тогда и только тогда, когда хотя бы одно из состояний множества Fвстречается бесконечно часто. Автоматы Бюхи используются в алгоритмах верификации методом проверки моделей.

1.8. Автоматные программы

Парадигма автоматного программирования предлагает мыслить о программе как о системе взаимодействующих автоматов и объектов управления (рисунок 1.8.1).

Рисунок 1.8.1. Автоматные программы

От внешней среды в автомат (A)приходят входные воздействия (переменные X₁и события e).Выходные воздействия автомата передаются объекту управления (ОУ). Объект управления обменивается данными (D_jи D₂)с внешней средой и подаёт на вход автомата переменные (X₂).

Выводы по главе 1

Описаны основные понятия, использующиеся в диссертации