Přístupnostní navigace
E-application
Search Search Close
Bachelor's Thesis
Author of thesis: Doubravka Šimůnková
Acad. year: 2025/2026
Supervisor: doc. RNDr. Milan Češka, Ph.D.
Reviewer: Ing. Roman Andriushchenko
Markov decision processes (MDPs) are fundamental models for sequential decision-making under uncertainty. A common task is to find a policy satisfying a given objective in a given MDP. However, at design time, one typically needs to consider a family of MDPs modelling various system variations. We aim to synthesise a policy tree, a structured decomposition of the family into subfamilies, each admitting its own robust policy. In this thesis, we integrate SMPMC — a method for finding robust policies using an SMT solver combined with probabilistic model checking — into an existing framework for synthesising policy trees, addressing two problems. First, (1) we use SMPMC as an alternative robust policy finder, exploiting its theoretical completeness to find robust policies where the original approach fails. Second, (2) we leverage SMPMC's ability to represent policies as decision trees to synthesise two-level decision trees, in which each leaf policy is itself a decision tree. Our evaluation shows that SMPMC's high computational cost limits its applicability to models with sufficiently small state spaces. However, on models where the original approach introduces spurious splits, our approach synthesises considerably more compact policy trees. For two-level decision tree synthesis, our approach produces trees significantly smaller than the baseline. Both contributions are implemented on top of PAYNT.
Markov Decision Processes, Families of MDPs, Decision Trees, Policy Trees, Robust Policies, SMT Solver, Model Checking
Date of defence
15.06.2026
Result of the defence
Defended (thesis was successfully defended)
Grading
C
Process of defence
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 C.
Topics for thesis defence
Language of thesis
English
Faculty
Fakulta informačních technologií
Department
Department of Intelligent Systems
Study programme
Information Technology (BIT)
Composition of Committee
doc. Ing. František Zbořil, Ph.D. (předseda) doc. Mgr. Kamil Malinka, Ph.D. (místopředseda) Ing. Jiří Matoušek, Ph.D. (člen) Ing. Vladimír Veselý, Ph.D. (člen) doc. Ing. Vítězslav Beran, Ph.D. (člen)
Supervisor’s reportdoc. RNDr. Milan Češka, Ph.D.
Celkově můžu konstatovat, že i) přes negativní výsledky byl hlavní cíle práce splněny, ii) většina textové části BP je na dobré úrovni a iii) studentka prokázal schopnost orientace a samostatné práce v netriviální problematice. Za předpokladu rozumné prezentace doporučuji tuto BP hodnotit stupněm B.
Jednalo se o středně obtížné zadání, které vyžadovalo pochopení pokročilých technik pro řešení rodin Markovských rozhodovacích procesů. Zadání umožňovalo poměrně široké možnosti realizace, ale studentka se dostala pouze k základnímu řešení.
Toto řešení realizuje požadovanou integraci uvážených metod (hlavní bod zadání), ale z mého pohledu mohlo být na BP odvedeno více práce (zejména návrh a implementace pokročilejší integrace). Přestože dosažené výsledky nesplnily naše očekávání, tj. navržená integrace zásadně nevylepšila existující přístupy, závěry této práce přinesly důležité poznatky pro další výzkum v této oblasti.
Práci s literaturou považuji za mírně nadprůměrnou. Studentka byla schopna použít doporučenou literaturu ke zpracování teoretické části a k celkové orientaci v tématu. Na druhou stranu studentka mohla aktivněji vyhledával alternativní zdroje a přístupy k danému problému (např. alternativní formulace SMT kódování pro hledaní rozhodovacích stromů).
Aktivita v průběhu řešení BP byla většinou dostatečná a studentka pravidelně reportovala a diskutovala dosažené výsledky. Výhradu mám k implementační (realizační) části BP, kde studentka často potřebovala pomoc od konzultanta – zde bych si přestavoval samostatnější přístup.
Ačkoliv realizační část byla dokončena poměrně pozdě, studentka byla schopna sepsat BP rychle a v dostatečné kvalitě. Proto větší část BP byla dostatečně konzultována a výsledná kvalita textu je velice dobrá.
Vzhledem k negativním výsledkům nemá současná podoba práce velký publikační potenciál. Na druhou stranu tato práce přinesla důležité poznatky a lze na ni dobře navázat a dosáhnout publikovatelné výsledky.
Grade proposed by supervisor: B
Reviewer’s reportIng. Roman Andriushchenko
Zadání práce bylo de facto splněno, i když nenaplnilo svůj potenciál. Implementační výstup je minimální, avšak funkční a důkladně otestovaný. Vzhledem k obtížnosti zadání a dobré kvalitě vypracované technické zprávy navrhuji hodnocení dobře (C).
Evaluation level: obtížnější zadání
Zadání práce vyžadovalo nastudování řady článků o induktivní syntéze pravděpodobnostních systémů, syntéze strategií pro množiny MDP a něco málo i o SMT solvingu, tj. témata mimo rozsah bakalářského studia.
Technická zpráva má vhodnou strukturu a jednotlivé kapitoly jsou informačně bohaté. Jedinou výhradou je Kapitola 4 (popisující navržená vylepšení), která by zasloužila větší pozornost. Oceňuji Kapitolu 5, pečlivě popisující testování navržené metody, a kapitoly 6-7 věnované důkladnému experimentálnímu hodnocení navržených vylepšení.
Práce je napsána výbornou angličtinou se zanedbatelným množstvím jazykových či typografických chyb.
Implementační výstup je funkční, avšak minimální: zahrnuje rozšíření (cca 100 LOC) logiky existující implementace AR a k tomu jeden modul obsahující jednu metodu (200 LOC) implementující rozhraní nad SMPMC nástrojem. Zdrojové kódy nejsou kvalitně zdokumentovány.
Experimentální výsledky mají smíšený charakter: použití SMPMC ke kontrole robustnosti typicky vede k výraznému zpomalení syntézy; na druhou stranu použití SMPMC k syntéze stromové reprezentace dané robustní strategie může vést k výraznému zmenšení výsledných stromů oproti stromům generovaným stávajícími technikami.
Evaluation level: zadání splněno pouze částečně s drobnými výhradami
Navržené řešení využívá techniku SMPMC založenou na SMT solvingu pro vylepšení standardní abstraction refinement (AR) smyčky dvěma způsoby: (1) na kontrolu existence jedné robustní strategie pro danou (pod)rodinu MDP a (2) na syntézu stromu reprezentujícího danou (prokazatelně robustní) strategii. Výsledkem syntézy je rozhodovací strom, který nejprve dělí množinu prostředí na třídy, kde každá třída je označena jednou robustní strategií ve formě rozhodovacího stromu. Oba způsoby však využívají SMPMC jednoduchým black-box způsobem: SMPMC nevyužívá externí znalosti z AR a ani AR nevyužívá diagnostické informace z SMPMC, např. pro lepší, informovanější rozdělení nejednoznačných rodin na podrodiny. Zadání tedy bylo de facto splněno, avšak nenaplnilo svůj potenciál, který vidím v ještě těsnější integraci obou přístupů pro generování hybridních stromů s proloženou klasifikací prostředí a klasifikací stavů.
Evaluation level: je v obvyklém rozmezí
V práci byla využita a správně ocitována relevantní literatura.
Grade proposed by reviewer: C
Responsibility: Mgr. et Mgr. Hana Odstrčilová