Побудова автомата Бюхі та алгоритми перевірки пустоти мови, яка акцептується автоматом, на основі BFS алгоритму

В ході виконання кваліфікаційної роботи було сформульовано загальні задачі і положення перевірки моделей, їх застосування в сучасній науці і техніці. Описано мову для для визначення властивостей безпеки і живучості, її загальні положення та алгоритм побудови узагальненого автомата Бюхі за ЛТЛ формулою. Введено основні поняття з перевірки моделей і перевірки автоматів на пустоту. Описано основні переваги та недоліки перевірки моделей.
Проведено аналіз існуючих алгоритмів для перевірки на пустоту, а саме алгоритми Емерсона-Лея та модифікований алгоритм Емерсона-Лея та алгоритми побудови автомата Бюхі за заданими специфікаціями.
Розроблено програмний продукт на основі технології С++, для верифікації моделі. Виконано порівняння ефективності алгоритмів, описано їх переваги і недоліки на різних вхідних даних.

Михайленко М. О. Побудова автомата Бюхі та алгоритми перевірки пустоти мови, яка акцептується автоматом, на основі BFS алгоритму : кваліфікаційна робота ... магістра
: 121 Інженерія програмного забезпечення / Михайленко Максим Олександрович. - Київ, 2021. - 66 с.