Thesis Details

Efficient Automata Techniques and Their Applications

Ph.D. Thesis Student: Havlena Vojtěch Academic Year: 2021/2022 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
Czech title
Efektivní automatové techniky a jejich aplikace

This thesis develops efficient techniques for finite automata and their applications. In particular, we focus on finite automata in network intrusion detection and automata in decision procedures and verification. In the first part of the thesis, we propose techniques of approximate reduction of nondeterministic automata decreasing consumption of resources of hardware-accelerated deep packet inspection. The second part is devoted to automata in decision procedures, in particular, to weak monadic second-order logic of k successors (WSkS) and the theory of strings. We propose a novel decision procedure for WS2S based on automata terms allowing one to effectively prune the state space. Further, we study techniques of WSkS formulae preprocessing intended to reduce the sizes of constructed intermediate automata. Moreover, we employ automata in a decision procedure of the theory of strings for efficient handling of the proof graph. The last part of the thesis then proposes optimizations in rank-based Buchi automata complementation reducing the number of generated states during the construction.


Finite automata, approximate reduction, minimization, tree automata, decision procedures, WSkS, automata terms, antiprenexing, theory of strings, quadratic word equations, Buchi automata complementation, rank-based complementation

Degree Programme
9 December 2021
HAVLENA, Vojtěch. Efficient Automata Techniques and Their Applications. Brno, 2021. Ph.D. Thesis. Brno University of Technology, Faculty of Information Technology. 2021-12-09. Supervised by Vojnar Tomáš. Available from:
    author = "Vojt\v{e}ch Havlena",
    type = "Ph.D. thesis",
    title = "Efficient Automata Techniques and Their Applications",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2021,
    location = "Brno, CZ",
    language = "english",
    url = ""
Back to top