Алгоритм перевірки пустоти мови, яка відповідає заданим специфікаціям лінійно темпоральної логіки й акцептується автоматами Бюхі, методом пошуку в глибину

В ходi виконання квалiфiкацiйної роботи було дослiджено складнiсть перевiрки пустоти мови автоматiв Бюхi за допомогою DFS алгоритмiв. Розглянута доцiльнiсть використання цiєї роботи в алгоритмах верифiкацiї автоматiв. Впродовж виконання квалiфiкацiйної роботи було проведено аналiз iснуючих алгоритмiв перевiрки пустоти, а саме алгоритми Nested та Two-stack. Дослiджено автоматичний пiдхiд до верифiкацiї моделей систем заданих LTL формулами.
Розроблено кросплатформний консольний продукт на основi технологiй C++ з використанням тiльки стандартної бiблiотеки шаблонiв (STL), призначений для перевiрки мови автоматiв на пустоту. Врахована можливiсть використання узагальнених автоматiв та їх перетворення для подальшого використання. Запропоновано алгоритм генерацiї довiльних автоматiв А.3. Виконано порiвняння ефективностi алгоритмiв на довiльних вхiдних даних.

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