Diplomová práce

Almost linear Bűchi automata

Bc. Tomáš Babiak, učo 143254
Anotace

V tejto práci sa zaoberáme špeciálnou triedou B\"{u}chiho automatov, ktorá sa volá Almost linear B\"{u}chi automata (ALBA) a jej vzťahom k fragmentu Lineárnej temporálnej logiky (LTL), ktorý sa nazýva LIO. V práci popisujeme preklad fragmentu LIO na ALBA a ukážeme jeho zložitosť. Ďalej porovnávame tento preklad s niekoľkými implementáciami štandardného prekladu logiky LTL na B\"{u}chiho automaty pomocou alternujúcich automatov.

Abstract

In this thesis, we are concerned in the special class of B\"{u}chi automata called Almost linear B\"{u}chi automata (ALBA) and its relation to the fragment of Linear temporal logic called LIO. We provide an effective translation of LIO to ALBA and show it complexity. Further we provide the comparison of this translation with some implementations of standard translation from LTL to B\"{u}chi automata via alternating automata.

Klíčová slova
Model-checking Linear temporal logic (LTL) LIO B\"{u}chi automata Almost linear B\"{u}chi automata (ALBA)
Zadání práce
Cílem práce je implementovat překlad fragmentu LTL zvaného LIO na téměř lineární Bűchiho automaty (ALBA). Překlad by měl být pokud možno optimalizován a porovnán se standardními překlady LTL do Bűchiho automatů ve smyslu rychlosti, spotřebované paměti a především velikosti a typu výsledného automatu. Porovnání bude provedeno na vzorku LTL formulí zahrnující formule z BEEMu a ze "Specification Patterns".
Administrativní informace
Práce zkontrolována:
12. 1. 2010 11:16, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
527,9 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
10. 2. 2010
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

prof. RNDr. Mojmír Křetínský, CSc., učo 631
KTP FI MU

Literatura

  • JAROŠ, Milan. Převod formulí LTL na automaty. Brno, 2003, iv, 60.
  • BABIAK, Tomáš; Vojtěch ŘEHÁK a Jan STREJČEK. Almost Linear Büchi Automata. In Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09). 1st ed. internet: EPTCS, 2009, s. 16-25. ISSN 2075-2180.
  • GASTIN, Paul a Denis ODDOUX. Fast LTL to Büchi Automata Translation. Edited by Gérard Berry - Hubert Comon - Alain Finkel. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01). Berlin: Springer-Verlag, 2001, s. 53-65. ISBN 3-540-42345-1.
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.

 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Tomáš Babiak FI N-IN PDS, učo 143254 cs3an/7
Babiak, T.
11. 1. 2010
Složky
Soubory
Anotace anglicky annotation_english.txt
Babiak, T.
11. 1. 2010
Anotace česky annotation.txt
Babiak, T.
11. 1. 2010
Content_of_the_CD.zip
Babiak, T.
11. 1. 2010
Klíčová slova keywords.txt
Babiak, T.
11. 1. 2010
posudek_oponenta.pdf
Křetínský, M.
4. 2. 2010
thesis.pdf
Babiak, T.
11. 1. 2010

  • 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.