Original title: Abstrakce Jazyků Stavů v Automatových Algoritmech
Translated title: Abstraction of State Languages in Automata Algorithms
Authors: Chocholatý, David ; Síč, Juraj (referee) ; Holík, Lukáš (advisor)
Document type: Bachelor's theses
Year: 2022
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Prověřujeme možnosti použití různých abstrakcí jazyků konečných automatů pro optimalizaci automatových algoritmů používaných pro rozhodování založené na automatech. Zajímáme se o abstrakci jazyků stavů na množiny přijímaných délek slov nebo Parikovy obrazy, reprezentované jako semi-lineární množiny, a zkoumáme možnosti jejich využití k optimalizaci automatových konstrukcí odstraňováním stavů založeném na abstrakcích jejich jazyků. Předvádíme několik abstrakcí a pracujeme na optimalizaci jejich výkonu. Používáme dva běžné automatové problémy, synchronní produkt konstrukci a rozhodování prázdnosti průniku konečných automatů, jako operace pro experimentální vyhodnocení, na kterých testujeme naše optimalizace. Naše abstrakce jsou nicméně aplikovatelné na mnohé další typické automatové operace, například generaci doplňku aj. Provedené experimenty ukazují, že navrhované optimalizace podstatně zmenšují generovaný stavový prostor pro oba testované problémy. We explore possibilities of using various abstractions of finite automata languages in optimization of automata algorithms used in automata reasoning. We focus on abstracting languages of states to sets of accepted lengths of word or Parikh images, represented as semi-linear sets, and explore options of using them to optimize automata constructions by pruning states based on abstractions of their languages. We propose several abstractions and work on optimizing their performance. We use two common finite automata problems, synchronous product construction and deciding the emptiness of finite automata intersection, as benchmark problems on which we test our optimizations. Nevertheless, our abstractions are applicable on many other typical automata operations, e.g., complement generation etc. Our experiments show that the proposed optimizations reduce generated state space for both benchmark problems substantially.
Keywords: abstrakce jazyků stavů; délková abstrakce; konečné automaty; konstrukce produktu; mintermizace; optimalizace výpočtu průniku; Parikovy obrazy; redukce stavového prostoru; SMT výpočty; test prázdnosti; emptiness test; finite automata; intersection computation optimization; length abstraction; mintermization; Parikh images; product construction; SMT solving; state language abstractions; state space reduction

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/207393

Permalink: http://www.nusl.cz/ntk/nusl-504935


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses