Rigorózní práce

Linear Temporal Logic and omega-automata

Mgr. František Blahoudek
Anotace

Teze mé dizertační práce se věnují aktivní oblasti výzkumu -- překladu Lineární Temporální Logiky (LTL) do deterministických automatů nad nekonečnými slovy (deterministických omega-automatů). V literatuře můžeme nalézt dva možné přístupy k překladu: překlad přímý a dvojkrokový překlad, který zahrnuje determinizaci Büchiho automatů. Teze popisují aktuální stav výzkumu v obou větvích, připomínají problémy …více

Abstract

This proposal of my Ph.D. thesis is dedicated to a currently active area of research -- translation of Linear Temporal Logic (LTL) into deterministic omega-automata (i.e. automata over infinite words). Two approaches to the translation can be found in the literature: direct translations and two-step translation including determinization of non-deterministic Büchi automata. This thesis proposal describes …více

Klíčová slova
LTL omega-automata linear temporal logic model checking
Administrativní informace
Práce zkontrolována:
1. 3. 2015 23:00, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
786,6 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
25. 5. 2015
Práce byla úspěšně obhájena

Oponenti

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU
RNDr. Jan Kofroň, Ph.D.
MFF UK v Praze
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.