Thesis Details
Abstraction in Automata Algorithms
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
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, doc. 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
@bachelorsthesis{FITBT24926, 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 = "https://www.fit.vut.cz/study/thesis/24926/" }