Disertační práce

Translation of Linear Temporal Logic to Omega-Automata

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

Překlad logiky lineárního času (Linear Temporal Logic - LTL) na různé typy ɷ-automatů je intenzivně studovaná oblast, která má mnoho aplikací. Metoda LTL ověřovaní modelu (LTL model checking) je rozšířená a plně automatizovaná technika, která se používá k ověření, zda daný systém splňuje požadovanou specifikaci. Jedním z klíčových kroků je překlad logiky LTL na Büchiho automaty. Různé vlastnosti, jako …více

Abstract

Translation of Linear Temporal Logic (LTL) into ɷ-automata of various types is a heavily studied area with wide range of applications. The translation of LTL formulae into Büchi automata represents one of the crucial steps for LTL model checking, a wide-spread fully-automated technique used to verify whether a given system satisfies a desired specification. Properties, such as size and determinism …více

Klíčová slova
LTL linear temporal logic model checking translation of LTL Buchi automata omega-automata deterministic automata Rabin automata HOA format
Administrativní informace
Práce zkontrolována:
3. 1. 2017 10:37, prof. RNDr. Mojmír Křetínský, CSc., učo 631
Plný text práce
2,3 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
28. 2. 2017
Práce byla úspěšně obhájena

Vedoucí

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

Oponenti

prof. RNDr. Petr Jančar, CSc.
ext FI MU, FEI VŠB-TU Ostrava
doc. Mgr. Adam Rogalewicz, Ph.D.
abs FI MU, FIT VUT v Brně
Prof. Dr. Javier Esparza
TU München

Konzultant

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika (čtyřleté)
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.