Disertační práce

Automata for Formal Methods: Little Steps Towards Perfection

RNDr. František Blahoudek
Anotace

Jako vhodná reprezentace jazyků nekonečných slov jsou ω-automaty hojně využívány ve formálních metodách. Obzvlášťe algoritmy, které analyzují systémy vykazující nekonečné chování, často spoléhají na ω-automaty. Díky efektivním algoritmům pro průnik, sjednocení a test prázdnosti reprezentovaných jazyků pro různé třídy ω-automatů jsou tyto automaty vhodné pro metody ověřování modelu se specifikací zadanou …více

Abstract

As ω-automata are a convenient representation of languages of infinite words, they are widespread in the area of formal methods; many algorithms that analyze systems with infinite behaviours rely on ω-automata. The efficient algorithms for the intersection, union, and emptiness checking for various classes of ω-automata made them appealing for model checking of properties expressed as ω-regular languages …více

Klíčová slova
ω-automata Büchi automata model checking deterministic automata complementation LTL linear temporal logic
Administrativní informace
Práce zkontrolována:
17. 3. 2018 10:41, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
3,1 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
25. 6. 2018
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponenti

Prof. Orna Kupferman
School of Computer Science and Engineering, Hebrew University
Prof. Christel Baier
Faculty of Informatics, TU Dresden
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.