Diplomová práce

Translation of an LTL fragment to deterministic Rabin and Streett automata

Bc. František Blahoudek
Anotace

Překlad LTL na deterministické omega-automaty se obvykle skládá z překladu na nedeterministické Buchiho automaty a jejich následné determinizace, např. Safrovou konstrukcí. V této diplomové práci je popsán překlad LTL fragmentu LTL(F, G) na deterministické automaty pomocí lineárních alternujících automatů speciálního tvaru, tzv. must/may automatů. Výslednými automaty jsou generalizované Rabinovy automaty …více

Abstract

The usual translation of LTL into deterministic omega-automata consists of translation to non-deterministic Buchi automata and determinization of such automata by some general algorithm such as Safra’s construction. In this thesis we describe a translation of the LTL fragment LTL(F, G) to deterministic automata via a special kind of very weak alternating automata called must/may automata. We use transition …více

Klíčová slova
Linear Temporal Logic (LTL) omega-automata infinite words alternating automata determinization
Zadání práce
Cílem práce je navrhnout překlad fragmentu LTL, který pracuje pouze s temporálními operátory F (eventually) a G (always), na deterministické Rabinovy a Streettovy automaty s akceptováním na hranách. Součásti práce bude i srovnání velikosti výsledných automatů s automaty produkovanými nástrojem ltl2dstar. Dále by práce měla vysvětlit možná využití výsledných automatů.
Administrativní informace
Práce zkontrolována:
29. 5. 2012 14:16, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
362 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
26. 6. 2012
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

  • PERRIN, Dominique a Jean-Éric PIN. Infinite words :automata, semigroups, logic and games. 1st ed. Amsterdam: Elsevier, 2004, xi, 538 s. ISBN 0-12-532111-2.
  • KRÖGER, Fred a Stephan MERZ. Temporal logic and state systems. Berlin: Springer, 2008, xi, 433. ISBN 9783540674016.
  • 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.

Podobné práce
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce František Blahoudek FI N-IN PDS kr9t4/6
Kryštofová, H.
26. 4. 2012
Složky
Soubory
Anotace anglicky annotation_english.txt
Blahoudek, F.
28. 5. 2012
Anotace česky annotation.txt
Blahoudek, F.
28. 5. 2012
Klíčová slova keywords.txt
Blahoudek, F.
28. 5. 2012
Plný text práce thesis.pdf
Blahoudek, F.
28. 5. 2012
Posudek oponenta posudek_oponenta.pdf
Křetínský, M.
19. 6. 2012

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