Thesis Details

Next Generation of Rank-Based Algorithms for Omega Automata

Bachelor's Thesis Student: Šmahlíková Barbora Academic Year: 2021/2022 Supervisor: Lengál Ondřej, Ing., Ph.D.
Czech title
Nová generace rank-based algoritmů pro omega automaty
Language
English
Abstract

Büchi automata (BA) complementation is a crucial operation for termination analysis of programs, model checking, or decision procedures for various logics. Despite its prominence, practically efficient algorithms for BA complementation are still missing. This thesis deals with optimizations of Büchi automata complementation, focusing mainly on rank-based techniques. The original rank-based algorithm is asymptotically optimal, but it can still generate unnecessarily large state space. For a practical usage, it is therefore desirable to reduce the number of generated states in the complement as much as possible. We propose several techniques that can efficiently complement some special types of Büchi automata, occuring often in practice, based on their structure. Some of these techniques can also, to a certain degree, be extended to general Büchi automata. The developed techniques were implemented as an extension of the tool Ranker for Büchi automata complementation and evaluated on thousands of hard automata. Our optimizations significantly reduce the generated state space and Ranker produces in the majority of cases a~smaller complement than other state-of-the-art tools.

Keywords

Büchi Automata, Büchi Complementation, Rank-Based Complementation, Elevator Automata

Department
Degree Programme
Files
Status
defended, grade A
Date
13 June 2022
Reviewer
Committee
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
Citation
ŠMAHLÍKOVÁ, Barbora. Next Generation of Rank-Based Algorithms for Omega Automata. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Lengál Ondřej. Available from: https://www.fit.vut.cz/study/thesis/24442/
BibTeX
@bachelorsthesis{FITBT24442,
    author = "Barbora \v{S}mahl\'{i}kov\'{a}",
    type = "Bachelor's thesis",
    title = "Next Generation of Rank-Based Algorithms for Omega Automata",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/24442/"
}
Back to top