Přístupnostní navigace
E-application
Search Search Close
Bachelor's Thesis
Author of thesis: Bc. Veronika Molnárová
Acad. year: 2022/2023
Supervisor: doc. Ing. Ondřej Lengál, Ph.D.
Reviewer: Ing. Vojtěch Havlena, Ph.D.
A finite state automaton is a mathematical model used to describe a machine that performs a computation on the given input over a series of states. In the last century, it has found many uses in different fields of information technology, from video game character behavior to compilers. While each automaton denotes its language, one language can be represented by an infinite number of different automata. As these automata vary in size, to ensure the most efficient work with them, we want to find the smallest one possible. In this thesis, we are going to look at five different types of automata reductions. Firstly, we will talk about three known reduction algorithms, which are the minimization of deterministic automata, the reduction based on a relation of simulation, and the reduction by transformation into a canonical residual automaton. These reductions were implemented in C++ and tested on a sample set of automata to compare their results. Lastly, we looked at the possibility of reducing finite state automata using Boolean satisfiability problem (SAT) and quantified Boolean formula (QBF) solvers. We are presenting a set of rules for each solver for generating a clause in conjunctive normal form (CNF), which can precisely represent the given automaton in Boolean algebra. We used this fact to create a new method of nondeterministic automata reduction.
finite state automata, automata reduction, minimal deterministic automata, simulation, residual automata, SAT solver, QBF solver
Date of defence
15.06.2023
Result of the defence
Defended (thesis was successfully defended)
Grading
A
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 A.
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
prof. Ing. Tomáš Vojnar, Ph.D. (předseda) doc. Ing. Petr Matoušek, Ph.D., M.A. (člen) Ing. František Grézl, Ph.D. (člen) doc. Ing. Tomáš Martínek, Ph.D. (člen) Ing. Matěj Grégr, Ph.D. (člen)
Supervisor’s reportdoc. Ing. Ondřej Lengál, Ph.D.
Jako vedoucí jsem byl s prací Veroniky Molnárové spokojen. Zadání bylo těžší, ale Veronika se s ním dokázala velmi dobře vypořádat a získala zajímavé výsledky, které budou sloužit pro další výzkum. Práci hodnotím stupněm výborně (A).
Zadání práce zapadá do oblasti výzkumu efektivních algoritmů pro manipulaci s konečnými automaty, který probíhá ve skupině VeriFIT. Jde o náročnější zadání, studentka si musela nastudovat řadu nových formalismů a algoritmů pro redukci konečných automatů, tyto implementovat, a poté ještě vymyslet nový způsob redukce automatů pomocí QBF solverů. S výsledky jsem spokojen - určitě by je šlo ještě vylepšit, ale to už by bylo nad rámec rozumných požadavků pro rozsah bakalářské práce.
Studentka dostala zadány základní materiály, zbytek si našla sama.
Konzultace probíhaly pravidelně, Veronika na ně chodila připravena.
Práce byla dokončena v rozumném předstihu.
Práce byla prezentována formou posteru na studentské konferenci EXCEL@FIT'23. Z výstupů je potenciál vytvořit článek na nějaké středně rozumné mezinárodní konferenci (což se doufám stane, byť si uvědomuji, že hlavní brzda je nedostatek času vedoucího).
Grade proposed by supervisor: A
Reviewer’s reportIng. Vojtěch Havlena, Ph.D.
Práci hodnotím známkou A - výborně. Jedná se o zdařilou práci přinášející nové výsledky. Technická zpráva je na velmi dobré úrovni. Oceňuji formální úroveň práce a rovněž kvalitní experimentální vyhodnocení, které přináší, pro mě, někdy dokonce až trošku překvapivé výsledky.
Evaluation level: obtížnější zadání
Zadání považuji za obtížnější. Práce vyžadovala nastudování různých aktuálních technik redukce konečných automatů, SAT a QBF solvingu a jejich efektivní implementace.
Evaluation level: zadání splněno
Zadání bylo kvalitně splněno.
Evaluation level: je v obvyklém rozmezí
Rozsah technické zprávy odpovídá vykonané práci a je v obvyklém rozmezí. Jednotlivé kapitoly jsou informačně bohaté a navazují na sebe. Práce neobsahuje zbytečné části.
Technická zpráva je po prezentační stránce velice pěkná. Práce je dobře čitelná a snadno pochopitelná. Jednotlivé pojmy jsou formálně definovány a jsou doplněny o příklady a neformální popis. Trošku více úsilí bych věnoval způsobu označování Boolovských proměnných pro přechody v navrženém algoritmu (aktuálně to působí trošku zmatečně). Navržený přístup redukce pomocí SAT/QBF je jinak velice dobře popsán, včetně komentáře jednotlivých rozhodnutí, což obvzláště oceňuji.
Práce je psaná dobrou angličtinou. Po typografické stráce se rovněž jedná o zdařilé dílo.
Práce cituje řadu aktuálních článků relevantních k tématu. Převzaté prvky jsou dle mého názoru řádně odlišeny od vlastních výsledků.
Programové řešení obsahuje program a skripty pro redukci konečných automatů. Ačkoliv zdrojové kódy nejsou nejrozsáhlejší, jsou dokumentované a je k dispozici readme pro snadné zprovoznění. Programové řešení mi bylo prezentováno a je funkční.
Práce přináší nové poznatky v oblasti redukce konečných automatů. Navržené algoritmy by mohly být zahrnuty do knihovny pro práci s automaty, kde by mohly rozšířit portfolio redukčních technik.
Grade proposed by reviewer: A
Responsibility: Mgr. et Mgr. Hana Odstrčilová