Алгоритм перевірки пустоти мови, яка відповідає заданим специфікаціям лінійно темпоральної логіки й акцептується автоматами Бюхі, методом пошуку в глибину
Дата
2021
Автори
Гальченко Максим
Назва журналу
ISSN журналу
Назва тому
Видавець
Анотація
В ход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дних даних.
Бібліографічний опис
Галузь знань та спеціальність
12 Інформаційні технології , 121 Інженерія програмного забезпечення
Бібліографічний опис
Гальченко М. Алгоритм перевірки пустоти мови, яка відповідає заданим специфікаціям лінійно темпоральної логіки й акцептується автоматами Бюхі, методом пошуку в глибину : кваліфікаційна робота ... магістра : 121 Інженерія програмного забезпечення / Максим Гальченко. - Київ, 2021. - 64 с.