Thesis Details

Abstraction in Automata Algorithms

Bachelor's Thesis Student: Kocourek Tomáš Academic Year: 2021/2022 Supervisor: Holík Lukáš, doc. Mgr., Ph.D.
Czech title
Abstrakce v automatových algoritmech

The goal of this thesis is to implement and experimentally compare antichain-based algorithms with and without abstraction, which decide the emptiness of alternating finite automata. The author also proposes his own algorithms using abstraction and comes up with a few optimizations of existing abstract algorithms. The thesis introduces the theoretical background of studied algorithms and describes efficient ways to implement data structures which are used by these algorithms. The experimental evaluation over random automata shows that the algorithms without abstraction give us better results in general because they do not perform costly evaluation of closed set intersection and complementation. However, in case of automata with high transition density, the algorithms without abstraction tend to decelerate, while the abstract ones accelerate.


alternating finite automaton, abstraction, antichain, language emptiness, concrete domain, abstract domain, fixed point, partition

Degree Programme
defended, grade B
13 June 2022
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, Ing., Ph.D. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
KOCOUREK, Tomáš. Abstraction in Automata Algorithms. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Holík Lukáš. Available from:
    author = "Tom\'{a}\v{s} Kocourek",
    type = "Bachelor's thesis",
    title = "Abstraction in Automata Algorithms",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = ""
Back to top