Název:
Knihovna pro výpočet relací simulace na Büchiho automatech
Překlad názvu:
A Library for Computing Simulation Relations over Büchi Automata
Autoři:
Odvárka, Daniel ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce) Typ dokumentu: Bakalářské práce
Rok:
2022
Jazyk:
eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng][cze]
Tato práce popisuje téma simulací relací nad Büchiho automaty a využití těchto relací simulací. Relace simulací jsou důležité pro snižování stavového prostoru automatů, nebo dále pro kontrolu pod aproximace jazykové inkluze. Dále popisujeme téma paritních her, které je úzce spojeno s výpočtem relací simulací pro některé typy simulací. Podívame se také na různé algoritmy pro řešení relací simulací. Zmíněné algoritmy byly implementovány v jazyce C++ a implementace byla porovnána s nástrojem RABIT. Z experimentů je vidno, že je naše implementace lepší pouze pro menší automaty.
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.
Klíčová slova:
Büchi automata; finite automata; parity games; reduction of an automaton; simulation relations; Büchiho automaty; konečné automaty; paritní hry; redukce automatu; relace simulací
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: http://hdl.handle.net/11012/207250