Diplomová práce

Complementation of TBA Based on Semi-Determinization

Bc. Mikuláš Klokočka
Anotace

Tato diplomová práce se věnuje tématu komplementace Büchiho automatů. V první řadě ukazuje již existující metody komplementace. Práce poté definuje nový algoritmus pro komplementaci nazvaný PBS. Dále uvadí řadu optimalizací tohoto algoritmu. Součástí této práce je taktéž jeho implementace. PBS je porovnáno s několika moderními nástroji pro komplementaci. Výsledky tohoto porovnání svědčí o tom, že je PBS konkurenceschopný.

Abstract

This thesis deals with the topic of complementation of Büchi automata. First, it shows a brief overview of the existing methods for complementation. Then it defines a new algorithm for complementation called PBS. It also covers a number of optimizations for this algorithm. Part of this thesis is also the implementation of PBS. PBS was compared to state-of-the-art tools for complementation. The results of this comparison indicate that PBS is competitive.

Klíčová slova
Büchi automata complementation model-checking
Zadání práce
The goal of this thesis is to propose and implement a new algorithm for complementation of transition-based Büchi automata (TBA). The algorithm should combine the ideas of algorithms for semi-determinization of TBA and for complementation of semi-deterministic automata. The thesis will also provide proof of correctness, complexity analysis of the produced automata, and experimental comparison of the implemented algorithm against other standard complementation algorithms.
Administrativní informace
Práce zkontrolována:
21. 5. 2019 11:06, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
561,7 KB / soubor PDF
Přílohy (2)
Jazyk práce
angličtina angličtina
Termín obhajoby
20. 6. 2019
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponent

doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
KTP FI MU

Konzultant

RNDr. František Blahoudek, Ph.D.
abs FI MU

Literatura

  • BLAHOUDEK, František; Matthias HEIZMANN; Sven SCHEWE; Jan STREJČEK a Ming-Hsien TSAI. Complementing Semi-deterministic Büchi Automata. In Marsha Chechik, Jean-François Raskin. Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016. Berlin: Springer Berlin Heidelberg, 2016, s. 770-787. ISBN 978-3-662-49673-2. Dostupné z: https://doi.org/10.1007/978-3-662-49674-9_49.
  • BLAHOUDEK, František; Alexandre DURET-LUTZ; Mikuláš KLOKOČKA; Mojmír KŘETÍNSKÝ a Jan STREJČEK. Seminator: A Tool for Semi-Determinization of Omega-Automata. Online. In Thomas Eiter and David Sands. Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017). Neuveden: EasyChair, 2017, s. 356-367. ISSN 2398-7340. Dostupné z: https://doi.org/10.29007/k5nl.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.