Efektivní algoritmy pro práci s Büchiho automaty
Loading...
Date
Authors
ORCID
Advisor
Referee
Mark
C
Journal Title
Journal ISSN
Volume Title
Publisher
Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract
Cílem této práce je rozšířit existující knihovnu VATA o modul pro práci s Büchiho automaty, které se řadí mezi konečně stavové automaty nad nekonečnými slovy. Tyto automaty jsou využívány v různých oblastech informatiky, mimo jiné také ve formální verifikaci, při LTL model checkingu. LTL model checking se provádí typicky za pomocí operace testování jazykové inkluze mezi dvěma Büchiho automaty. Protože jazyková inkluze může být výpočetně velmi náročná, vzniklo několik optimalizovaných algoritmů pro tento problém, jako je například přístup založený na Ramseyho větě. Předkládaná práce je zaměřena na tento přístup, jehož implementace je přidána do nově vytvořeného rozšíření knihovny VATA. Mimo to jsou do tohoto nového rozšíření přidány také další operace nad Büchiho automaty, jako jsou sjednocení, průnik nebo redukce počtu stavů.
The main goal of this work is to extend the existing library VATA with a module for working with Büchi automata, which are finite state automata over infinite words. These automata are used in many areas of computer science, among others in formal verifications, namely in LTL model checking. LTL model checking is typically carried out using the operation of testing language inclusion between two Büchi automata. Because testing language inclusion can be computationally very demanding, several optimized algorithms have been created for testing language inclusion such as the Ramsey-based approach. This work is focused on the mentioned approach, the implementation of which is added to the newly created extension of the VATA library. Apart from that, the new extension adds additional useful operations over Büchi automata such as union, intersection or a reduction in the number of states.
The main goal of this work is to extend the existing library VATA with a module for working with Büchi automata, which are finite state automata over infinite words. These automata are used in many areas of computer science, among others in formal verifications, namely in LTL model checking. LTL model checking is typically carried out using the operation of testing language inclusion between two Büchi automata. Because testing language inclusion can be computationally very demanding, several optimized algorithms have been created for testing language inclusion such as the Ramsey-based approach. This work is focused on the mentioned approach, the implementation of which is added to the newly created extension of the VATA library. Apart from that, the new extension adds additional useful operations over Büchi automata such as union, intersection or a reduction in the number of states.
Description
Citation
LAŠČÁK, T. Efektivní algoritmy pro práci s Büchiho automaty [online]. Brno: Vysoké učení technické v Brně. Fakulta informačních technologií. 2014.
Document type
Document version
Date of access to the full text
Language of document
cs
Study field
Informační technologie
Comittee
prof. RNDr. Alexandr Meduna, CSc. (předseda)
doc. Ing. Zdeněk Kotásek, CSc. (místopředseda)
Ing. František Grézl, Ph.D. (člen)
Ing. Martin Hrubý, Ph.D. (člen)
RNDr. Marek Rychlý, Ph.D. (člen)
Date of acceptance
2014-06-18
Defence
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm C. Otázky u obhajoby: Jak konkrétně zlepšit výkon testu inkluze? Je algoritmus na straně 25 správně? Pokud ne, co je třeba opravit?
Result of defence
práce byla úspěšně obhájena
Document licence
Standardní licenční smlouva - přístup k plnému textu bez omezení