Thesis Details
Next Generation of Rank-Based Algorithms for Omega Automata
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.
Büchi Automata, Büchi Complementation, Rank-Based Complementation, Elevator Automata
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{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/" }