Detail práce
Hledání řídicích strategií pomocí UPPAAL STRATEGO
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení.
formální verifikace, ověřování modelů, časované automaty, modální logika, dotazovací jazyk, Uppaal, Uppaal SMC, Uppaal Stratego, řídicí strategie
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 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 C.
- Je použití nástroje vhodné pro danou aplikaci?
- Zkusil jste použít jiné existující heuristiky na řešení dané úlohy?
Drahanský Martin, prof. Ing., Dipl.-Ing., Ph.D. (UITS FIT VUT), člen
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Hrubý Martin, Ing., Ph.D. (UITS FIT VUT), člen
Polčák Libor, Ing., Ph.D. (UIFS FIT VUT), člen
@bachelorsthesis{FITBT22413,
author = "Filip Hru\v{s}ka",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Hled\'{a}n\'{i} \v{r}\'{i}dic\'{i}ch strategi\'{i} pomoc\'{i} UPPAAL STRATEGO",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2020,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/22413/"
}