Diplomová práce

Translation of LTL to Semi-Deterministic Automata via Alternating Automata

Bc. Michal Románek
Anotace

Cieľom tejto práce je preklad LTL formulí na Semi-deterministické automaty (sDBA) skrz veľmi slabé alternujúce automaty a porovnanie výsledného nástroja s ostatnými existujúcimi nástrojmi na preklad LTL do sDBA.

Abstract

The goal of this thesis is to translate LTL formulae to Semi-deterministic Automata (sDBA) via Very Weak Alternating Automata and compare the resulting tool with other existing tools for translation of LTL into sDBA.

Klíčová slova
LTL alternating automata semi-deterministic automata
Zadání práce
Cílem práce je navrhnout, popsat a implementovat překlad LTL formulí na semi-deterministické automaty (semi-deterministic TGBA) přes velmi slabé alternující automaty (VWAA), přičemž překlad LTL na VWAA již existuje a lze využít beze změn. Součástí práce bude porovnání vzniklého nástroje s jinými nástroji pro překlad LTL na semi-deterministické automaty (ltl2ldba a Spot+Seminator).
Administrativní informace
Práce zkontrolována:
22. 5. 2018 16:13, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
75,5 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
22. 6. 2018
Práce nebyla obhájena
Student v rámci svého studia diplomovou práci obhájil 4. 2. 2019.

Vedoucí

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

Oponenti

doc. RNDr. Pavel Matula, Ph.D., učo 2927
KVI FI MU
prof. RNDr. Ivana Černá, CSc., učo 1419

Konzultant

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

Literatura

  • BABIAK, Tomáš; Mojmír KŘETÍNSKÝ; Vojtěch ŘEHÁK a Jan STREJČEK. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan, Barbara König. TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012, s. 95-109. ISBN 978-3-642-28755-8. Dostupné z: https://doi.org/10.1007/978-3-642-28756-5_8.
  • 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
Aplikovaná 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.