Přístupnostní navigace
E-application
Search Search Close
Master's Thesis
Author of thesis: Ing. Ondrej Alexaj
Acad. year: 2025/2026
Supervisor: doc. Ing. Ondřej Lengál, Ph.D.
Reviewer: Ing. Michal Hečko
Complementation of ω-automata is a notoriously difficult operation that, in the worst case, incurs a doubly exponential state blow-up. As observed in other computationally hard problems, such as SAT, practical handling of such complexity often relies on heuristics or on specialized constructions tailored to restricted but relevant subclasses. In this thesis, we follow this approach and develop a specialized complementation procedure for elevator automata, a subclass of transition-based Emerson-Lei automata expressive enough to capture all ω-regular languages and naturally arising in practical applications. Our experimental results indicate that this direction is promising: on elevator-automata benchmarks, the proposed construction often produces substantially smaller automata than the current state-of-the-art tool.
ω-automata, complementation, language inclusion, emptiness checking, elevator automata, TELA, formal verification
Date of defence
22.06.2026
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 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í studenta 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 and Artificial Intelligence (MITAI)
Specialization
Mathematical Methods (NMAT)
Composition of Committee
doc. Mgr. Adam Rogalewicz, Ph.D. (předseda) doc. RNDr. Milan Češka, Ph.D. (místopředseda) Ing. Martin Hrubý, Ph.D. (člen) Ing. Aleš Smrčka, Ph.D. (člen) Dr. Ing. Petr Peringer (člen) Ing. Jaroslav Rozman, Ph.D. (člen)
Supervisor’s reportdoc. Ing. Ondřej Lengál, Ph.D.
Diplomová práce Ondreje Alexaje je pěkným završením několika let jeho předchozí práce na daném tématu. Výsledky práce posouvají stav poznání v oblasti práce s omega-automaty a to jak na teoretické, tak i na praktické úrovni. Dvě přijaté publikace jen potvrzují technickou hloubku dosažených výsledků. S diplomovou prací Ondreje Alexaje jsem velmi spokojen a z pozice vedoucího ji hodnotím známkou A.
Práce byla značně náročná, jelikož vyžadovala posunutí současného stavu poznání v oblasti praktické i teoretické práce s automaty pro omega-regulární jazyky. Práce navazuje na omega-automatový výzkum skupiny VeriFIT. S výsledky jsem velmi spokojen---jedna část práce se materializovala přijatým článkem na konferenci CAV'26 (CORE A*) a druhá část práce zase článkem přijatým na konferenci CONCUR'26 (od letoška CORE B, dlouho předtím CORE A).
Práce byla dokončena v dostatečném předstihu, finální obsah dostatečně konzultován.
Jak již bylo řečeno, část práce byla přijata k publikaci na konferenci CAV'26 (CORE A*) a druhá část byla přijata na konferenci CONCUR'26 (CORE B). Práce byla dále prezentována na studentské soutěži Excel@FIT 2026, kde byla oceněna odborným panelem. O výsledky práce mají zájem např. prof. Strejček z FI MUNI nebo prof. Duret-Lutz z Laboratoire de Recherche de l'Epita v Paříži.
Student dostal zadanou relevantní literaturu, další zdroje si našel sám.
Student pravidelně konzultoval, na konzultace chodil připravený, dodržoval dohodnuté termíny.
Grade proposed by supervisor: A
Reviewer’s reportIng. Michal Hečko
The thesis addresses a highly technical and challenging topic and presents it in a clear and accessible manner. The theoretical contributions, including the development of complementation procedures for Emerson–Lei elevator automata together with their complexity analyses, are remarkable. Furthermore, these algorithms have been implemented in the open-source tool Kofola. Extensive experimental evaluation demonstrates that Kofola produces significantly smaller automata than the current state of the art.
A publication co-authored by the student and based on the presented research is already under review for CONCUR 2026 (CORE B), further underscoring the relevance and quality of the work.
The student has also been actively collaborating with his supervisor on research related to automata over infinite words for several years. This sustained commitment to the research area is noteworthy and helps explain the exceptional quality of the achieved results.
Based on the above, I would like to nominate the student for any award for which this thesis is eligible.
Evaluation level: zadání splněno a práce obsahuje podstatná rozšíření
The results obtained in this thesis are extraordinary. The primary contribution is an extension of the complementation procedure for so-called elevator automata, demonstrating how to handle arbitrary Emerson–Lei acceptance conditions. This is a remarkable result, as an Emerson–Lei acceptance condition is a formula with arbitrary Boolean structure specifying which acceptance atoms must be satisfied infinitely or finitely often along a run. To convey the significance of this achievement, Emerson–Lei acceptance subsumes all standard acceptance conditions. Consequently, the algorithm developed in this thesis yields, as special cases, complementation procedures for elevator automata equipped with classical acceptance conditions.
Other notable contributions include a procedure for converting an arbitrary Emerson–Lei automaton into an elevator automaton and an extension of the complementation procedure for initially almost deterministic accepting components from Büchi acceptance to arbitrary Emerson–Lei acceptance conditions. The excellence of the thesis is further highlighted by the fact that some of the presented results are currently under review for publication at CONCUR 2026 (CORE B).
Evaluation level: přesahuje obvyklé rozmezí
The main body of the thesis comprises 65 pages of technical material written to an exceptionally high standard.
The thesis is very well written. Although the subject matter is highly technical and complex, the results are presented in an accessible manner, progressing from simpler models to the general case and thereby helping the reader build intuition.
Both the typographical and linguistic quality of the thesis are at the level of a high-quality scientific publication.
The student has surveyed an extensive body of scientific literature on Büchi automata and algorithms for their manipulation. References are used appropriately throughout the thesis, clearly positioning the work within the broader research context.
The thesis is accompanied by an impressive implementation of the proposed algorithms as part of the open-source tool Kofola. The implementation underwent extensive experimental evaluation on benchmarks arising, among others, from HyperLTL model checking. The results demonstrate that the proposed algorithms produce substantially smaller automata than the current state-of-the-art approach.
The part of the thesis devoted to the complementation of Emerson–Lei elevator automata is already under review for publication at CONCUR 2026 (CORE B), further highlighting the scientific quality and impact of the work.
Evaluation level: značně obtížné zadání
The assignment is highly challenging. Its core formalism consists of Büchi automata, which are automata accepting infinite words; consequently, proofs and algorithms involving this model are often complex and require familiarity with specialized mathematical concepts and modes of reasoning. Furthermore, the problems addressed in the assignment are of considerable practical importance, particularly in the analysis and verification of reactive systems. These problems are also known to be computationally difficult. Over the years, numerous techniques, heuristics, and optimization methods have been proposed and evaluated experimentally. As a result, identifying novel and practically useful heuristics is inherently challenging. Any such contribution therefore represents an advancement in the scalability and efficiency of the underlying approach.
Grade proposed by reviewer: A
Responsibility: Mgr. et Mgr. Hana Odstrčilová