Thesis Details

Abstraction of State Languages in Automata Algorithms

Bachelor's Thesis Student: Chocholatý David Academic Year: 2021/2022 Supervisor: Holík Lukáš, doc. Mgr., Ph.D.
Czech title
Abstrakce Jazyků Stavů v Automatových Algoritmech

We explore possibilities of using various abstractions of finite automata languages in optimization of automata algorithms used in automata reasoning. We focus on abstracting languages of states to sets of accepted lengths of word or Parikh images, represented as semi-linear sets, and explore options of using them to optimize automata constructions by pruning states based on abstractions of their languages. We propose several abstractions and work on optimizing their performance. We use two common finite automata problems, synchronous product construction and deciding the emptiness of finite automata intersection, as benchmark problems on which we test our optimizations. Nevertheless, our abstractions are applicable on many other typical automata operations, e.g., complement generation etc. Our experiments show that the proposed optimizations reduce generated state space for both benchmark problems substantially.


finite automata, state language abstractions, SMT solving, product construction, emptiness test, intersection computation optimization, state space reduction, length abstraction, Parikh images, mintermization

Degree Programme
defended, grade A
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
CHOCHOLATÝ, David. Abstraction of State Languages 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 = "David Chocholat\'{y}",
    type = "Bachelor's thesis",
    title = "Abstraction of State Languages in Automata Algorithms",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = ""
Back to top