Detail práce
Efektivní funkcionální knihovna pro konečné automaty
Konečné automaty jsou důležitou matematickou abstrakcí. Ve formální verifikaci se konečné automaty používají ke stručné reprezentaci regulárních jazyků. V této souvislosti se používají operace nad konečnými automaty, jako je testování jazykové univerzality a inkluze. Naivní přístup k implementaci těchto operací vede k explicitní determinizaci konečného automatu, což může být nakladné a nežádoucí. Nicméně existuje pokročilejší metoda k vykonávání těchto operací nazývaná Antichains algoritmus, která se vyhýbá explicitní determinizaci. Tato práce se zabývá efektivní implementací operací nad konečnými automaty v Haskellu a také porovnává několik implementačních variant. Získané výsledky jsou poté porovnány s knihovnou VATA, což je imperativní implementace knihovny pro práci nad konečnými automaty.
konečné automaty, antichain, knihovna, funkcionální jazyk, Haskell, lazy evaluace
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm B - velmi dobře.
- Uveďte nějakou z výhod Vaší knihovny oproti knihovně VATA.
- Proč jste k experimentůn použil pouze 20 automat?
Čadík Martin, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT ČVUT), člen
Orság Filip, Ing., Ph.D. (UITS FIT VUT), člen
Zachariášová Marcela, Ing., Ph.D. (UPSY FIT VUT), člen
@mastersthesis{FITMT19561,
author = "Jakub \v{R}\'{i}ha",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Efektivn\'{i} funkcion\'{a}ln\'{i} knihovna pro kone\v{c}n\'{e} automaty",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2017,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/19561/"
}