Detail práce
Knihovna pro konečné automaty a převodníky
Konečné automaty majú široké uplatnenie v informatike, okrem iných vo formálnej verifikácii, modelovaní systémov a spracovaní prirodzeného jazyka. Avšak modely skutočne reprezentujúce realitu bývajú veľmi komplikované a môžu byť definované nad veľkými, v niektorých prípadoch až nekonečnými, abecedami, a teda môžu obsahovať veľký počet prechodov. V týchto prípadoch nemusí byť je použitie algoritmov na prácu s konečnými automatmi efektívne. Symbolické automaty poskytujú stručnejší zápis tak, že namiesto symbolov v prechodoch používajú predikáty. Konečné prevodníky tiež majú široké uplatnenie, od ligvistiky až po formálnu verifikáciu. Symbolické prevodníky nahradzujú symboly dvojicou predikátov - jeden predikát pre vstupné symboly a jeden pre výstupné. Cieľom tejto práce je návrh knižnice pre klasické a symbolické automaty a prevodníky, ktorá bude vhodná na rýchle prototypovanie nových algoritmov.
konečné automaty, symbolické automaty, transducery, efektívne algoritmy, formálna verifikácia
Studentka nejprve prezentovala výsledky, kterých dosáhla v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Studentka následně odpověděla na otázku 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í studentky na položené otázky rozhodla práci hodnotit stupněm výborně A.
- Jak by bylo složité rozšířit knihovnu o podporu symbolických automatů v plné míře (aspoň pro základní množinové operace, tj. průnik, sjednocení, komplement) za použítí externího SMT solveru pro formule predikátové logiky prvního řádu?
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT), člen
Novák Michal, doc. RNDr., Ph.D. (UMAT FEKT VUT), člen
Strnadel Josef, Ing., Ph.D. (UPSY FIT VUT), člen
Szőke Igor, Ing., Ph.D. (UPGM FIT VUT), člen
@bachelorsthesis{FITBT20123,
author = "Michaela Bielikov\'{a}",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Knihovna pro kone\v{c}n\'{e} automaty a p\v{r}evodn\'{i}ky",
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/20123/"
}