Bachelor's thesis

Transformation of Nondeterministic Büchi Automata to Tight Automata

Marek Jankola
Abstract

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

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

Keywords
Büchi automata model checking ω-automata shortest counterexample tight Büchi automata
Thesis description
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.
Administrative information
The thesis has been checked:
27/5/2021 12:17, prof. RNDr. Jan Strejček, Ph.D., UČO 3366
Full text of thesis
1023,4 KB / file PDF
Attachments (1)
Language used
English English
Defence date
29/6/2021
The thesis was defended successfully

Supervisor

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

Reader

prof. RNDr. Jiří Barnat, Ph.D., UČO 3496
KTP FI MU
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics
Field of Study

Theses on a related topic

List of theses with an identical keyword.

Similar documents

  • 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.