Přístupnostní navigace
E-application
Search Search Close
Master's Thesis
Author of thesis: Ing. Filip Macák
Acad. year: 2022/2023
Supervisor: doc. RNDr. Milan Češka, Ph.D.
Reviewer: doc. Mgr. Lukáš Holík, Ph.D.
This work focuses on combining two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making under uncertainty. A central issue is to find a POMDP controller that achieves a total expected reward objective. As finding optimal controllers is undecidable, we concentrate on synthesising good finite-state controllers (FSCs). We do so by tightly integrating two modern, orthogonal methods for POMDP controller synthesis: a belief-based and an inductive approach. The former method obtains an FSC from a finite fragment of the so-called belief MDP, an MDP that keeps track of the probabilities of equally observable POMDP states. The latter is an inductive search technique over a set of FSCs with a fixed memory size. The key result of this work is a symbiotic anytime algorithm that tightly integrates both approaches such that each profits from the controllers constructed by the other. Experimental results indicate a substantial improvement in the value of the controllers while significantly reducing the synthesis time and memory footprint.
Markov models, probabilistic models, automated synthesis, model checking, formal methods, partial observability
Date of defence
21.06.2023
Result of the defence
Defended (thesis was successfully defended)
Grading
A
Process of defence
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 přítomných, např. ohledně významu pojmu "kontroler" a jejich rozsahu, postupu pro nacházení kontrolerů či charakteru použité optimalizační metody. 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 výborně / A.
Language of thesis
English
Faculty
Fakulta informačních technologií
Department
Department of Intelligent Systems
Study programme
Information Technology and Artificial Intelligence (MITAI)
Specialization
Mathematical Methods (NMAT)
Composition of Committee
doc. Dr. Ing. Petr Hanáček (předseda) doc. RNDr. Milan Češka, Ph.D. (člen) Ing. Martin Hrubý, Ph.D. (člen) doc. Mgr. Kamil Malinka, Ph.D. (člen) Ing. Matěj Grégr, Ph.D. (člen) Mgr. Ing. Pavel Očenášek, Ph.D. (člen)
Supervisor’s reportdoc. RNDr. Milan Češka, Ph.D.
Vzhledem k obtížnému zadání, samostatné práci a dosaženým výsledkům, které zásadně přispěly k publikaci na prestižních konferenci, navrhuji hodnotit tuto DP známkou A. Jelikož kvalita prezentace a odbornost textu DP je na vynikající úrovni a dosažené výsledky vylepšují state-of-art ve velice aktuální a důležité oblasti (bezpečné a škálovatelné řízení agentů v nejistém prostředí), navrhuji práci ocenit cenou děkana a nominovat ji do užšího výběru pro soutěž IT SPY.
Jedná se o náročné zadaní s výzkumným zaměřením, které vyžadovalo nastudování pokročilých technik z oblasti formálních metod pro pravděpodobnostní systémy včetně detailního pochopení pokročilých implementačních postupů. DP práce vznikala v rámci projektu s mezinárodní spoluprací. Student se velice rychle zorientoval v dané problematice a rychle začal přispívat do projektu. Zadání bylo splněno a s dosaženými výsledky jsou velice spokojen (viz níže).
Student se samostatně a velmi kvalitně seznámil s existující literaturou a rovněž z existujícími implementacemi syntetizačních algoritmů.
Student byl velice aktivní po celou dobu řešení projektu a DP, dodržoval dohodnuté termíny a dostatečně konzultoval svůj postup. Velice oceňuji, že student pracoval samostatně a prokázal schopnost se sám zorientovat v relativně obtížné a pro studenta nové oblasti.
Přestože se student významně podílel na přípravě publikace (viz níže), zvládl realizační i textovou část DP dokončit včas a tak mohla být výsledná podoba DP dostatečně konzultována. Mohu však konstatovat, že předložený text byl dobře logicky strukturován a
celková kvalita prezentace DP byla na vynikající úrovni -- toto demonstruje schopnost studenta samostatně vypracovat kvalitní odborný text.
Student se zásadním způsobem podílel na přípravě publikace (je jedním ze spoluautorů), která stojí na výsledcích jeho DP a byla nedávno přijata na prestižní konferenci CAV’23 (CORE rank A*, poměr přijatých článku kolem 25 %). Student se zásadně podílel na formulaci hlavních myšlenek, návrhu algoritmu a sepisování článku. Dále byl zodpovědný z implementaci a experimentální vyhodnocení. Tudíž mohu objektivně konstatovat, že tento článek by bez Filipa Macáka tento rok určitě nevznikl.
Grade proposed by supervisor: A
Reviewer’s reportdoc. Mgr. Lukáš Holík, Ph.D.
Student odvedl extrémně kvalitní práci, a to po stránce celkového objemu práce, zvládnutí náročné problematiky, kreativního řešení problémů, implementace, i prezentace. Vše toto je doloženo přijetím práce na konferenci CAV, která je špičkou v oblasti formálních metod.
Je třeba dodat, že student pracoval obklopen aktivním týmem vědeckých pracovníků, kteří mají s výzkumem v oblasti velké zkušenosti, a není možné mu přičíst všechen kredit za dosažený výsledek. Původní myšlenka, technická řešení, i text článku, ze ktrého diplomová práce čerpá, jsou společným dílem. Studentův přínos byl ale nadstandardní a klíčový, zejména po stránce nalezení a implementace technických řešení, experimentálního vyhodnocení, a podílel se výrazně na všech aspektech práce, včetně formulace textů článku. Lze říci, že práce dosáhla současného úspěchu zejména díky jeho přispění.
Navrhuji zvážit všemožná ocenění, např. IT SPY, nejen pro kvalitu zpracování, ale i pro její relevanci k výzkumného směru obecně a také v rámci výzkumných projektů na FIT.
Evaluation level: značně obtížné zadání
Zadán byl výzkumný cíl v oblasti syntézy POMDP, která staví na komplexním a poměrně rozsáhlém matematickém aparátu, jehož zvládnutí přesahuje možnosti běžného studenta FIT. Cíl je natolik ambiciózní, že jeho dosažení vedlo k publikaci na špičkové konferenci CAV. Fakt, že se jedná o práci týmu seniorních vědeckých pracovníků obtížnost tématu posouvá do zvládnutelné roviny, požadavky na studenta byly ale stále velmi vysoké.
Evaluation level: zadání splněno a práce obsahuje podstatná rozšíření
Kvalita výsledku dosáhla úrovně špičkové mezinárodní publikace a daleko přesahuje požadavky na diplomovou práci. Přijetí práce na konferenci CAV, podmíněné velmi pozitivní odezvou tří předních odborníků v oblasti, mluví za vše, a považuji jej za kredibilnější referenci než svůj vlastní názor (nejsem odborníkem v oblasti syntézy POMDP). Budu se proto níže vyjadřovat spíše stručně a spíše k formálním aspektům práce.
Evaluation level: je v obvyklém rozmezí
Celý text se po všech stránkách výrazně neodchyluje od kvality zmíněné konferenční publikace.
Viz prezentační úroveň technické zprávy.
Realizačním výstupem je implementace nového algoritmu syntézy, kombinací nástrojů STORM a PAYNT. Jedná se o poměrně rozsáhlou implementaci komplikovaných algoritmů, která byla pečlivě experimentálně vyhodnocena. Výsledky jasně demonstrují, že nový algoritmus produkuje kvalitnější výsledky, a navíc rychleji, než dříve existující metody a nástroje. Opět by mělo stačit říci, že realizační výstup hrál zásadní roli pro přijetí práce na konferenci CAV.
Výsledky jsou využitelné v syntéze POMDP a jako základ dalšího výzkumu a rozvoje v oblasti.
Výsledky mají potenciál dasáhnou ohlasu ve vědecké komunitě, jedná se o současně intezinvě zkoumanou oblast s velkým praktickým potenciálem.
Grade proposed by reviewer: A
Responsibility: Mgr. et Mgr. Hana Odstrčilová