|
|
Transducers in Automata Library Mata
Chocholatý, David ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Implementujeme konečné převodníky do nové rychlé a jednoduché automatové knihovny Mata. Konečné převodníky jsou konečné stavové stoje modelující regulární relace. Naše hlavní použití pro konečné převodníky je kódovaní operací nahrazení (nahrazení slova nebo regulárního vzoru řetězcem). Nový SMT nástroj pro řešení formulí s omezeními nad řetězci Z3-Noodler používá knihovnu Mata jako základ pro jeho rozhodovací proceduru. Noodler potřebuje konečné převodníky k analýze programů manipulujících s řetězci s operacemi nahrazení. Analýzou zmíněných programů používaných ve webových aplikacích se zabrání útokům jako cross-site scripting (XSS) nebo vložení kódu. Hlavní odlišující vlastnosti knihovny Mata zahrnují jednoduchost (jednoduchá k užívání, úpravě a rozšíření) a efektivitu (pracuje rychle). Reprezentaci a algoritmy pro konečné převodníky jsme navrhli s ohledem na tyto vlastnosti knihovny. K reprezentaci konečných převodníků a jejich algoritmů znovupoužijeme a rozšíříme existující datové struktury a algoritmy pro konečné automaty v knihovně Mata. Reprezentace pro konečné převodníky slouží jako společná reprezentace pro konečné převodníky a budoucí reprezentaci automatů využívajících multi-terminálních binárních rozhodovacích diagramů pro práci s velkými abecedami. Navíc rozšíříme návrh o algoritmy pro konstrukci konečných převodníků modelujících operace nahrazení definovaných v SMT-LIB. Nakonec experimentálně vyhodnotíme efektivitu konečných převodníků v knihovně Mata na nové sadě příkladů s operacemi nahrazení z běhů nástroje Z3-Noodler a z řešení problémů nalezení vzoru.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (referee) ; Holík, Lukáš (advisor)
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.
|
|
|
Regulated Language Operations and Their Use
Chocholatý, David ; Kožár, Tomáš (referee) ; Meduna, Alexandr (advisor)
This thesis introduces and studies erasing systems as an alternative formal language model to general jumping finite automata. A significant difference compared to the given automata is the use of a control regular language instead of state control in the form of a general finite automaton. Erasing systems leave the string work on the input tape, whereas regular languages themselves can be accepted by classical finite automata. At the same time, with the introduction of a new formal system, the thesis demonstrates its relations with well-known language families, the family of shuffle languages, Dyck languages and closure properties. Based on the formal specification of the erasing system, multiple applications in bioinformatics for molecular biology, text editors and compositional chess are shown, including designing algorithms and presenting the implementation solution.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (referee) ; Holík, Lukáš (advisor)
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.
|
guest ::
