Bakalářská práce

Transformation of Nondeterministic Büchi Automata to Tight Automata

Marek Jankola
Anotace

Model checking je technika, ktorá slúži na overenie, či naprogramovaný systém spĺňa danú vysokoúrovňovú špecifikáciu. V prípade, že ju nespĺňa, model checker vráti protipríklad. Avšak tento protipríklad nemusí byť najkratší možný. Existuje špeciálny typ Büchiho automatu – tight Büchiho automat, z ktorého dokáže model checker vždy vrátiť najkratší protipríklad. Cieľ tejto práce je navrhnúť algoritmus …více

Abstract

Model checking is a technique to verify whether a programmed system satisfies a given high-level specification or not. If it does not meet the specification, the model checker returns a counterexample. However, this counterexample might not be the shortest. There is a specific type of Büchi automaton - tight Büchi automaton from which the model checker can always return the shortest counterexample …více

Klíčová slova
Büchi automata model checking ω-automata shortest counterexample tight Büchi automata
Zadání práce
Cílem práce je navrhnout algoritmus transformující nedeterministické Büchiho automaty (NBA) na ekvivalentní tight NBA, které se využívají například při ověřování modelu (model checking) k získání nejkratšího protipříkladu. Součástí práce bude analýza složitosti tohoto algoritmu. Text bude doplněn vhodnými příklady.
Administrativní informace
Práce zkontrolována:
27. 5. 2021 12:17, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
1023,4 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
29. 6. 2021
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU
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.