Detail práce
Next Generation of Rank-Based Algorithms for Omega Automata
Komplementace Büchiho automatů je klíčovou operací pro terminační analýzu programů, model checking nebo rozhodovací procedury pro různé logiky. Tato práce se zabývá především optimalizacemi rank-based komplementace Büchiho automatů. Původní rank-based algoritmus je sice asymptoticky optimální, přesto může generovat nezbytně velký stavový prostor. Pro praktické použití je tedy žádoucí maximálně redukovat počet vygenerovaných stavů v komplementu. V této práci představíme několik technik pro efektivní komplementaci některých speciálních typů Büchiho automatů, často se vyskytujících v praxi, které jsou založené na jejich struktuře. Některé z navržených technik lze do určité míry rozšířit i pro obecné Büchiho automaty. Techniky představené v této práci byly implementovány jako rozšíření nástroje Ranker pro komplementaci Büchiho automatů. Tyto optimalizace výrazně redukují generovaný stavový prostor a Ranker ve většině případů produkuje menší komplement než ostatní existující nástroje pro komplementaci.
Büchiho automaty, Komplementace Büchiho automatů, Rank-based komplementace, Elevator automaty
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á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í studentky na položené otázky rozhodla práci hodnotit stupněm A.
1) The comparison focuses on sizes, the gains are visible. Although the gains in numbers of timeouts are also notable and very nice, time is not in the focus of the comparison. Are there arguments that sizes are more important than times? Are there plans to compare times?
2) In section 6.3.1., the end, you talk about 485 elevator automata. How much of these are random/LTL? Are the following experiments done only with these 485 formulas?
3) How much of the tool is your work?
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Martínek Tomáš, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT), člen
@bachelorsthesis{FITBT24442,
author = "Barbora \v{S}mahl\'{i}kov\'{a}",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Next Generation of Rank-Based Algorithms for Omega 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/24442/"
}