Кривий Сергій Лук’яновичМихайленко Максим Олександрович2023-03-202024-05-142023-03-202021Михайленко М. О. Побудова автомата Бюхі та алгоритми перевірки пустоти мови, яка акцептується автоматом, на основі BFS алгоритму : кваліфікаційна робота ... магістра : 121 Інженерія програмного забезпечення / Михайленко Максим Олександрович. - Київ, 2021. - 66 с.https://ir.library.knu.ua/handle/123456789/2849В ході виконання кваліфікаційної роботи було сформульовано загальні задачі і положення перевірки моделей, їх застосування в сучасній науці і техніці. Описано мову для для визначення властивостей безпеки і живучості, її загальні положення та алгоритм побудови узагальненого автомата Бюхі за ЛТЛ формулою. Введено основні поняття з перевірки моделей і перевірки автоматів на пустоту. Описано основні переваги та недоліки перевірки моделей. Проведено аналіз існуючих алгоритмів для перевірки на пустоту, а саме алгоритми Емерсона-Лея та модифікований алгоритм Емерсона-Лея та алгоритми побудови автомата Бюхі за заданими специфікаціями. Розроблено програмний продукт на основі технології С++, для верифікації моделі. Виконано порівняння ефективності алгоритмів, описано їх переваги і недоліки на різних вхідних даних.uaМагістерська робота