Master's thesis

Almost linear Bűchi automata

Bc. Tomáš Babiak, UČO 143254
Abstract

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.

Keywords
Model-checking Linear temporal logic (LTL) LIO B\"{u}chi automata Almost linear B\"{u}chi automata (ALBA)
Thesis description
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".
Administrative information
The thesis has been checked:
12/1/2010 11:16, prof. RNDr. Jan Strejček, Ph.D., UČO 3366
Full text of thesis
527,9 KB / file PDF
Language used
English English
Defence date
10/2/2010
The thesis was defended successfully

Supervisor

prof. RNDr. Jan Strejček, Ph.D., UČO 3366
KTP FI MU

Reader

prof. RNDr. Mojmír Křetínský, CSc., UČO 631
KTP FI MU

Literature

  • JAROŠ, Milan. Převod formulí LTL na automaty. Brno, 2003, iv, 60.
  • BABIAK, Tomáš; Vojtěch ŘEHÁK and 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, p. 16-25. ISSN 2075-2180.
  • GASTIN, Paul and 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, p. 53-65. ISBN 3-540-42345-1.
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics
Field of Study

Theses on a related topic

List of theses with an identical keyword.

 
Name
Posted by
Uploaded/Created
Rights
Archive of Thesis/Dissertation Tomáš Babiak FI N-IN PDS, učo 143254 cs3an/7
Babiak, T.
11/1/2010
Folders
Files
Abstract (in English) annotation_english.txt
Babiak, T.
11/1/2010
Abstract (in Czech) annotation.txt
Babiak, T.
11/1/2010
Content_of_the_CD.zip
Babiak, T.
11/1/2010
Keywords 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.