Bakalářská práce

Mapping the Omega-Automata Jungle

Tomáš Macháček
Anotace

Automaty na nekonečných slovech byly zavedeny před 60 lety. V průběhu let se staly klíčovou součástí oblastí, jako jsou formální verifikace, syntéza modelů a oblasti formálních metod obecne. Spolu s novými případy použití bylo představeno mnoho nových typů Büchiho automatů. Cílem této práce je shromáždit definice různých typů Büchiho automatů, kategorizovat tyto typy do hierarchie a uvést pro ně známé případy použití.

Abstract

Automata on infinite words were introduced 60 years ago. Over the years they became a key part of areas like formal verification, model synthesis and formal methods in general. Along with new use cases, many new types of Büchi automata were introduced. The focus of this thesis is to collect definitions of various Büchi automata types, categorize these types into hierarchy, and list typical use cases for them.

Klíčová slova
Büchi automata ω-automata Büchi automata hierarchy model checking
Zadání práce
cílem práce je zmapovat používané typy omega-automatů (přičemž důraz bude kladen na strukturální vlastnosti spíše než na akceptační podmínku) a popsat vztahy a možné převody mezi nimi. Práce by dále měla zmínit typická využití jednotlivých typů automatů a podporu těchto typů v existujících nástrojích.
Administrativní informace
Práce zkontrolována:
16. 12. 2022 11:45, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
490,6 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
31. 1. 2023
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

Dr. rer. nat. Achim Blumensath, učo 237782
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Informatika

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.