Master's thesis

Reductions of TGBA by Advanced Simulations

Redukcie TGBA pomocou pokročilých simulácií

Bc. Tatiana Zbončáková
Abstract

V tejto diplomovej práci predstavujeme spôsob ako rozšíriť definíciu priamej doprednej, oneskorenej doprednej a priamej spätnej simulácie na zovšeobecnené Büchiho automaty s akceptáciou na hranách (TGBA). Pre každú z navrhnutých simulácií sme dokázali, že kvocient TGBA na základe ekvivalencie podľa tejto simulácie, zachováva jazyk TGBA. Súčasťou práce je aj návrh a implementácia algoritmu na výpočet …more

Abstract

In this thesis, we present a way how to extend definitions of direct forward, delayed forward, and direct backward simulation relations for transition-based generalized Büchi automata (TGBA). For each of the proposed simulations, we prove that TGBA quotienting based on the equivalence according to this simulation preserves the language of automaton. We also present and implement an algorithm to compute …more

Keywords
TGBA SPOT omega-automat simulačné relácie kvocientovanie paritná hra redukcia priama dopredná simulácia oneskorená dopredná simulácia priama spätná simulácia
Thesis description
The goal of this thesis is to extend the simulation-based automata reductions designed by Clemens and Mayr for (state-based) Büchi automata (BA) to transition-based generalized Büchi automata (TGBA). The thesis focuses primarily on the delayed simulation as TGBA reductions based on direct simulations (both forward and backward) are already implemented in Spot. The subgoals of this thesis are as follows:
  • The definition of delayed simulation will be extended to TGBA.
  • It will be proven that TGBA quotienting under the symmetric closure of this simulation produces an equivalent TGBA.
  • An algorithm for computation of the simulation will be suggested and implemented.
  • The TGBA reduction by quotienting will be also implemented.
  • There will be an experimental evaluation showing whether the implemented reduction can further reduce the automata already reduced by Spot.
The implemetation will be done on top of the Spot library.
Administrative information
The thesis has been checked:
8/1/2021 09:46, prof. RNDr. Jan Strejček, Ph.D., UČO 3366
Full text of thesis
436,9 KB / file PDF
Attachments (2)
Language used
Slovak Slovak
Defence date
8/2/2021
The thesis was defended successfully

Supervisor

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

Reader

doc. RNDr. Vojtěch Řehák, Ph.D., UČO 3721
KTP FI MU

Consultant

RNDr. Juraj Major, UČO 396325
CVT FI MU
Cite this text
Masaryk University Faculty of Informatics
Programme
Applied 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.