Doctoral thesis

Automata for Formal Methods: Little Steps Towards Perfection

RNDr. František Blahoudek
Abstract

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 …more

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 …more

Keywords
ω-automata Büchi automata model checking deterministic automata complementation LTL linear temporal logic
Administrative information
The thesis has been checked:
17/3/2018 10:41, prof. RNDr. Jan Strejček, Ph.D., UČO 3366
Full text of thesis
3,1 MB / file PDF
Attachments (1)
Language used
English English
Defence date
25/6/2018
The thesis was defended successfully

Supervisor

prof. RNDr. Jan Strejček, Ph.D., UČO 3366
KTP FI MU

Readers

Prof. Orna Kupferman
School of Computer Science and Engineering, Hebrew University
Prof. Christel Baier
Faculty of Informatics, TU Dresden
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics (4-years)
Field of Study

Theses on a related topic

List of theses with an identical keyword.

Similar documents

  • Co je jinak přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Co je jinak další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Co je jinak pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Co je nové vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Co je nové 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.

  • Co se chystá

    Připravujeme další vylepšení pro mobilní zařízení.