Thesis Details

A Library for Computing Simulation Relations over Büchi Automata

Bachelor's Thesis Student: Odvárka Daniel Academic Year: 2021/2022 Supervisor: Lengál Ondřej, Ing., Ph.D.
Czech title
Knihovna pro výpočet relací simulace na Büchiho automatech
Language
English
Abstract

This thesis presents the topic of simulation relations over Büchi automata and the use case of various simulations. The simulation relations are important for reducing a state space of an automaton, or checking the under approximation of language inclusion. There are also parity games, which are important for computing some of the simulation types we introduce. We will go over multiple algorithms that compute these simulation relations. The mentioned algorithms are implemented in programming language C++ and are compared to a tool named RABIT. Our implementation is better only for smaller sized automata.

Keywords

finite automata, Büchi automata, simulation relations, parity games, reduction of an automaton

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade B
Date
13 June 2022
Reviewer
Holík Lukáš, doc. Mgr., Ph.D.
Committee
Janoušek Vladimír, doc. Ing., Ph.D. (DITS FIT BUT), předseda
Burget Lukáš, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Honzík Jan M., prof. Ing., CSc. (DIFS FIT BUT), člen
Mrázek Vojtěch, Ing., Ph.D. (DCSY FIT BUT), člen
Rozman Jaroslav, Ing., Ph.D. (DITS FIT BUT), člen
Citation
ODVÁRKA, Daniel. A Library for Computing Simulation Relations over Büchi 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/24439/
BibTeX 
@bachelorsthesis{FITBT24439,
    author = "Daniel Odv\'{a}rka",
    type = "Bachelor's thesis",
    title = "A Library for Computing Simulation Relations over B{\"{u}}chi 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/24439/"
}

Theses

Back to top