Náročnější výzkumné zadání, literaturou a charakterem technických/vědeckých problémů. Zadání bylo poměrně otevřené, přesná forma automatového modelu nebyla na začátku zřejmá.

Automatový model má potenciál posunout výkon string constraint solvingu a stát se tak základem publikace. 

Student byl aktivní a samostatný. Zadání zahrnovalo dlouhou fázi tápání, identifikaci formálního modelu a hledání hlavního směru řešení, kde byl student aktivní a konstruktivní, finální automatový model nebyl zřejmý, má smysl a má potenciál být velmi užitečný.
Fáze tápání měla poměrně široký záběr a vznikly kromě prezentované práce také zárodky řešení souvisejících problémů (například redukce velikosti pro prezentovaný automatový model). Hlavního úkolu, průzkumu hlavních teoretických vlastností modelu, zejména analýzy problému prázdnosti, se pak student zhostil samostatně a kompetentně, oceňuji návrh optimalizovaného testu prázdnosti, který sice zatím nepřináší zjevnou výhodu z pohledu složitosti, ale pravděpodobně bude mít zásadní praktický význam. Experimentální vyhodnocení je skromné, ale vzhledem k tomu, že hlavním cílem bylo identifikovat model a vyřešit základní teoretické problémy je možné jej považovat za plus. 

Evaluation level: zadání splněno a práce obsahuje podstatná rozšíření

Zadání bylo splněno---bylo vytvořeno rozšíření konečných automatů, které umožňuje exponenciálně kompaktnější reprezentaci některých regulárních jazyků než klasické konečné automaty a cílí na typ automatů objevující se během práce solveru Z3-Noodler. Nad rámec zadání bylo rozšíření prototypově implementováno a experimentálně zhodnoceno.

Prezentační úroveň technické zprávy je dobrá, kapitoly dávají smysl, navazují na sebe. Práce obsahuje detailní důkazy uvedených tvrzení (někdy možná příliš detailní, např. Tvrzení 5.6 je celkem zřejmé a u neformálního důkazy by nemuselo být potřeba jít do takové hloubky), které jsem detailně nezkoumal, ale na první pohled vypadají korektní.

Dokázal bych si představit, že by první část experimentálního porovnání (analýza automatů produkovaných Z3-Noodlerem) mohla být po kapitole 3 (úvod do nástroje Z3-Noodler), aby v tomto místě lépe motivovala vznik nového automatového modelu. Ocenil bych více demonstračních příkladů (např. v kapitole 4 u různých automatových modelů) nebo jejich lepší volba (např. pro příklad nového modelu automatu v obrázku 5.1 by bylo lepší zvolit něco, kde je úspora oproti klasickému konečnému automatu). Na straně 16 je chyba ve formální definici akceptační podmínky, která je naštěstí vyjasněna ihned následujícím intuitivnám popisem (ale může čtenáře zmást).

Některá Lemmata v kapitole 6 by bylo lepší uvést formálněji (např. Lemma 6.9, Lemma 6.10).

Sekce 6.2 a 6.3 (testování univerzality a redukce na základě simulace) jsou velmi krátké a celkem zbytečné, jelikož s nimi práce dále nepracuje. Sekce 6.3 definuje relaci přímé simulace na novém automatovém modelu jako základ pro redukci automatu. Tady si myslím, že pokud by se dělala simulační redukce dle této relace standardním způsobem, tak by byla nekorektní, jelikož tato relace dle mého názoru neimplikuje jazykovou inkluzi (např. u automatů s negovanými atomickými predikáty).

Práce cituje relevantní zdroje, citace jsou v pořádku. Myslím si, že hloubější studium technik pro analýzu (zobecněných) Rabinových či Emerson-Lei automatů by mohlo pomoci v sekci 6.1 při analýze silně souvislých komponent (např. článek "Baier, Blahoudek, Duret-Lutz, Klein, Müller, Strejcek: Generic Emptiness Check for Fun and Profit. ATVA 2019: 445-461" obsahuje techniky (a odkazy na další relevantní literaturu), které by mohlo být užitečné znát a případně použít). Na toto by však student sám asi těžko narazil.

Výsledky práce jsou využitelné v dalším rozšíření nástroje Z3-Noodler, avšak jejich smysluplné využití vyžaduje ještě dost práce (modifikace rozhodovací procedury nástroje Z3-Noodler). Po dotažení práce lze zvážit publikaci.