Master's Thesis

Lazy automata combination evaluation for regular model checking

Author of thesis: Ing. Le Duy Nguyen

Acad. year: 2025/2026

Supervisor: doc. Mgr. Lukáš Holík, Ph.D.

Abstract:

Regular model checking verifies infinite-state systems by representing configurations as words, sets of configurations as regular languages recognised by NFAs, and transitions by finite transducers; standard operations on these objects, like union, intersect, and most important one, complement, which can cause exponential blow-ups due to determinisation. This thesis proposes a lazy on-the-fly forward emptiness procedure for symbolic automata expressions that explores only the macrostates needed to answer the query instead of constructing product or powerset automata, and that prunes the search using subsumption pruning strengthened by simulation-based approximations. The framework is designed to be generic over NFA and NFT operators of arbitrary arity, length-preserving NFTs in the verified scope, and is therefore not restricted to regular model checking; this thesis evaluates it on a regular model checking benchmark suite as a representative use case, where it substantially outperforms existing explicit-construction baselines both in the number of solved instances and in the time taken on the instances they all solve.

Keywords:

regular model checking, nondeterministic finite automata, finite transducers, automata terms, lazy evaluation, on-the-fly exploration, antichains, subsumption, simulation preorder, determinization avoidance, reachability, emptiness checking, RMC, NFA, NFT

Date of defence

22.06.2026

Result of the defence

Defended (thesis was successfully defended)

znamkaAznamka

Grading

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

Have you considered how to utilise randomised subsumption pruning to consistently achieve better results across the majority of cases? Are there any insights that could help predict when to try subsumption and when not to?
Figure 4.1 is not described in the text at all. Could you explain the purpose of the figure and the figure itself (what exactly it shows) and its relevance to the presented work?
Have you explored the lazy evaluation capabilities of other state-of-the-art automata libraries, and whether they can be implemented in the proposed approach?
Is the lazy evaluation implemented in this work easily extensible to other use cases utilising the Mata automata library? Do you have ideas for future work where the proposed lazy evaluation implementation could be further used?

Language of thesis

English

Faculty

Fakulta informačních technologií

Department

Department of Intelligent Systems

Study programme

Information Technology and Artificial Intelligence (MITAI)

Specialization

Cybersecurity (NSEC)

Composition of Committee

doc. Mgr. Kamil Malinka, Ph.D. (předseda)
doc. Ing. Ondřej Ryšavý, Ph.D. (místopředseda)
Ing. Zbyněk Křivka, Ph.D. (člen)
doc. Ing. Ivan Homoliak, Ph.D. (člen)
Ing. Libor Polčák, Ph.D. (člen)
Ing. Radek Hranický, Ph.D. (člen)

Supervisor’s report
doc. Mgr. Lukáš Holík, Ph.D.

Samostatně zpracované náročnější téma, v kvalitě, s rozšířeními, které výkon řešení posouvají na úroveň, kdy si zaslouží publikaci.

Evaluation criteria	Verbal classification
Informace k zadání	Náročnější zadání, studentovo pojetí z něj dělá náročné zadání.
Aktivita při dokončování	Příkladná, vše dokončeno včas a konzultováno.
Publikační činnost, ocenění	Práce se pravděpodobně stane částí publikace a bude hrát důležitou roli ve spolupráci s TU Munich.
Práce s literaturou	Náročná technická literatura zpracována adekvátně.
Aktivita během řešení, konzultace, komunikace	Student byl velmi samostatný zejména ve fázi technického řešení práce. Práci zpracoval obecně velmi kvalitně a hlavně přišel s řadou zásadních a rozsáhlých optimalizací, které překvapivě posunuly výkon metody na ůroveň překonávající známé metody. Práce se tak může se stát základem pro publikaci. Kladně hodnotím také studentovu schopnost psát technický text.

Points proposed by supervisor: 95

Grade proposed by supervisor: A

Reviewer’s report
Ing. David Chocholatý

The thesis explores the lazy evaluation of finite automata/transducers and approaches to abstract regular model checking, analyses the design of the automata library Mata, and proposes a new lazy evaluation framework for the library. The proposed design is general and does not slow down the library. As the experimental evaluation demonstrates, the implemented design outperforms the currently used, well-optimised approaches utilising Mata in regular model checking and can be further expanded with additional features.

The student demonstrated his ability to explore a complex theoretical and practical problem, analyse the state of the art, design a solution, implement it, and experimentally evaluate the proposed design. Nevertheless, the presentation is polished, well-motivated and defined. The proposed approach is well implemented and experimentally evaluated. Only slight issues with the presentation and the content of the work, which, however, do not disrupt the reader's experience, can be found.

For these reasons, I give the thesis a strong A.

Evaluation criteria	Verbal classification	Points
Rozsah splnění požadavků zadání	Evaluation level: zadání splněno The thesis met all the requirements set out in the assignment.
Rozsah technické zprávy	Evaluation level: je v obvyklém rozmezí The thesis satisfies the length requirements. The chapters are well laid out, contain the expected information, and are relevant to the work.
Prezentační úroveň technické zprávy	The chapters are appropriately investigated. The text is comprehensible to the reader, and the flow is comfortable. Definitions and explanations are accompanied by illustrative examples with figures and diagrams. The motivation for the thesis is clearly explained, and the stated problems are answered in later chapters. However, the analysis of existing lazy-evaluation approaches could be more extensive. The experimental evaluation thoroughly explores the work. The benchmarks used are not characterised properly (e.g., what they look like and how large they are). Some experimental evaluation results could be better explained, especially regarding some (maybe surprising) outliers, and the conditions under which to use the random subsumption checking could be further investigated. The combination of optimisations could also be explored. Future work could be more clearly commented on.	93
Formální úprava technické zprávy	The thesis is well-written. The intuitive explanations are followed by formal definitions. The thesis contains only a few isolated, negligible stylistic and grammatical mistakes that do not disrupt the reader's experience. Some figures are placed around the paragraphs discussing them without an explicit reference (4.1, 4.3).	94
Práce s literaturou	All claims in the thesis are sufficiently supported by the cited works. Appropriate literature was chosen to support the claims. The referenced literature ranges from relevant theoretical and practical papers to general books about automata theory and regular model checking. The state of the art is thoroughly explored and cited.	95
Realizační výstup	The proposed design was implemented in the library Mata, tested, and evaluated. The implementation is generic, extensible, and backwards-compatible. Importantly, it does not hinder the performance of NFAs in Mata. The code is well-documented and easy to understand. The work is in the process of being integrated into the main branch of the Mata library. The code, as is, meets all the library's quality requirements and will be merged with only negligible modifications.	96
Využitelnost výsledků	The work extends the Mata library with new automata/transducer operations featuring lazy evaluation, using a mix of existing finite automata algorithms and implementing a lazy evaluation framework that utilises them. The support for lazy evaluation in Mata is crucial for the continuous development of tools that depend on Mata, notably regular model checking and string solving, where it solves existing performance bottlenecks. The results of the thesis are expected to be highly utilised from now on.
Náročnost zadání	Evaluation level: obtížnější zadání The student needed to study several research papers on regular model checking, finite automata and transducers, lazy evaluation approaches to operations on finite automata/transducers, and the automata techniques used by the automata library Mata. The student had to familiarise himself with the entire automata library Mata to understand how to utilise the most fundamental data structures and algorithms used in the library to add support for lazy evaluation capabilities for automata/transducers. For this reason, I consider this assignment to be more demanding than the average assignment.

Topics for thesis defence:

Have you considered how to utilise randomised subsumption pruning to consistently achieve better results across the majority of cases? Are there any insights that could help predict when to try subsumption and when not to?
Have you explored the lazy evaluation capabilities of other state-of-the-art automata libraries, and whether they can be implemented in the proposed approach?
Is the lazy evaluation implemented in this work easily extensible to other use cases utilising the Mata automata library? Do you have ideas for future work where the proposed lazy evaluation implementation could be further used?
Figure 4.1 is not described in the text at all. Could you explain the purpose of the figure and the figure itself (what exactly it shows) and its relevance to the presented work?

Points proposed by reviewer: 95

Grade proposed by reviewer: A

Responsibility: Mgr. et Mgr. Hana Odstrčilová

VUT

Faculties and university institutes

Parts

Lazy automata combination evaluation for regular model checking