Detail práce

A Library for Computing Simulation Relations over Büchi Automata

Bakalářská práce Student: Odvárka Daniel Akademický rok: 2021/2022 Vedoucí: Lengál Ondřej, Ing., Ph.D.
Název česky
Knihovna pro výpočet relací simulace na Büchiho automatech
Jazyk práce
anglický
Abstrakt

Tato práce popisuje téma simulací relací nad Büchiho automaty a využití těchto relací simulací. Relace simulací jsou důležité pro snižování stavového prostoru automatů, nebo dále pro kontrolu pod aproximace jazykové inkluze. Dále popisujeme téma paritních her, které je úzce spojeno s výpočtem relací simulací pro některé typy simulací. Podívame se také na různé algoritmy pro řešení relací simulací. Zmíněné algoritmy byly implementovány v jazyce C++ a implementace byla porovnána s nástrojem RABIT. Z experimentů je vidno, že je naše implementace lepší pouze pro  menší automaty.

Klíčová slova

konečné automaty, Büchiho automaty, relace simulací, paritní hry, redukce automatu

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Informační technologie
Soubory
Stav
obhájeno, hodnocení B
Obhajoba
13. června 2022
Oponent
Holík Lukáš, doc. Mgr., Ph.D.
Průběh obhajoby

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.

Otázky u obhajoby
  1. What is the primary source of your benchmarks? I.e., are they practically relevant? How? Or are they random?
  2. Why is Rabit so much faster on larger automata? Is it the algorithms themselves or the implementation?
  3. Why did you write your thesis in English?
Komise
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT), předseda
Burget Lukáš, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Honzík Jan M., prof. Ing., CSc. (UIFS FIT VUT), člen
Mrázek Vojtěch, Ing., Ph.D. (UPSY FIT VUT), člen
Rozman Jaroslav, Ing., Ph.D. (UITS FIT VUT), člen
Citace
ODVÁRKA, Daniel. A Library for Computing Simulation Relations over Büchi Automata. Brno, 2022. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2022-06-13. Vedoucí práce Lengál Ondřej. Dostupné z: https://www.fit.vut.cz/study/thesis/24439/
BibTeX 
@bachelorsthesis{FITBT24439,
    author = "Daniel Odv\'{a}rka",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "A Library for Computing Simulation Relations over B{\"{u}}chi Automata",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/24439/"
}

Závěrečné práce

Nahoru