Rigorózní práce

Translation of LTL to omega-automata

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

LTL overovanie modelu je široko rozšírená a plne automatizovaná technika, ktorá sa používaná na overenie, či daný systém spĺňa požadovanú špecifikáciu. Jedným z kľúčových krokov je preklad logiky LTL na Büchiho automaty. Vlastnosti výsledného automatu, ako sú veľkosť a determinizmus, majú veľký vplyv na výkon celej procedúry. Zlepšeniu tohto prekladu sa už venovalo veľa úsilia, napriek tomu majú dnešné …více

Abstract

LTL model checking is a wide-spread fully-automated technique used to verify whether a given system satisfies a desired specification. One of the crucial steps is a translation of LTL logic into Büchi automata. Properties, such as size and determinism, of a produced automaton can have a significant impact on the overall performance of the model checking procedure. Much effort was already devoted to …více

Klíčová slova
LTL linear temporal logic BA Büchi automata omega automata model checking translation of LTL
Administrativní informace
Práce zkontrolována:
22. 10. 2011 20:32, prof. RNDr. Mojmír Křetínský, CSc., učo 631
Plný text práce
392,7 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
10. 1. 2012
Práce byla úspěšně obhájena

Oponenti

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU
Dr. Alexandre Duret-Lutz
LRDE Cedex, France
Autor posudku dosud neidentifikován.
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.