Bakalářská práce

Transformation of Büchi Automata to Smaller Tight Automata

Karel Procházka
Anotace

Těsné automaty akceptují ultimátně periodická slova pomocí běhů se stejně dlouhou periodou a prefixem. Těsné automaty jsou užitečné například v ověřování modelu pro nalezení nejkratších protipříkladů. Tato práce upravuje konstrukci od Jankoly a Strejčka pro transformaci Büchiho automatů na ekvivalentní těsné Büchiho automaty, přičemž oproti původní konstrukci vytváří těsné automaty s menším počtem …více

Abstract

Tight automata are automata over infinite words that accept lasso-shaped (ultimately periodic) words with "shortest" possible runs. Tight automata are useful for example in model checking for finding the shortest counterexamples. This thesis modifies the construction by Jankola and Strejček that transforms Büchi automata into equivalent tight Büchi automata. The new construction produces tight automata …více

Klíčová slova
Büchi automata tight Büchi automata transition-based Büchi automata infinite words lasso-shaped ultimately periodic shortest counterexample model checking
Zadání práce
The goal of the thesis is to design and implement an improvement of the algorithm that transforms nondeterministic Büchi automata into equivalent tight Büchi automata presented in the paper "Tighter Construction of Tight Büchi Automata" and implemented in Tightener. More precisely, the improved algorithm should not add states and transitions to the resulting automata that are not needed for tightness. Hence, the resulting automata will be smaller than (or of the same size as) the tight Büchi automata produced by Tightener (when automata post processing is not considered). The improved algorithm will also decide whether a given automaton is tight. The thesis will contain an experimental comparison with existing tools.
Administrativní informace
Práce zkontrolována:
24. 5. 2025 16:57, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
747,8 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
23. 6. 2025
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

Literatura

  • JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Cham: Springer, 2024, s. 234-255. ISBN 978-3-031-57227-2. Dostupné z: https://doi.org/10.1007/978-3-031-57228-9_12.
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.