|
|
Heuristics in String Solving
Řezáč, Michal ; Havlena, Vojtěch (referee) ; Síč, Juraj (advisor)
Tato práce se zaměřuje na identifikaci heuristik a strategií použitých v moderních string solverech a na vyhodnocení jejich dopadu na efektivitu řešení. Zkoumány jsou především dva solvery – cvc5 a Z3. Práce popisuje techniky používané SMT solverech a strategie, které implementují string solvery. Vyhodnocení efektivity heuristik bylo prováděno jejich vypínáním přímo v kódu uvedených nástrojů a následným vyhodnocením dopadu na řešení standardních sad benchmarků. Výsledkem této práce je soupis sady konkrétních heuristik a popis struktury nástrojů cvc5 a Z3. Měřením se nepodařilo prokázat, jak velký skutečný dopad identifikované a popsané heuristiky mají.
|
|
|
Finding Weaknesses of Hyperscan
Hrabovský, Jiří ; Vojnar, Tomáš (referee) ; Síč, Juraj (advisor)
Cilem této bakalářské práce je vysvětlit, jak funguje open source vyhledávač regulárních výrazů Hyperscan, a poskytnutí přehledu algoritmů, které interně používá. Druhým cílem je pomocí experimentů zjistit, jak moc lze ovlivnit výkon Hyperscanu skenovaným textem. Na základě zdrojového kódu a článků od autorů Hyperscanu je v kapitole 3 vysvětleno, jak Hyperscan vyhledává regulární výrazy v textu a v kapitole 4 jsou vysvětleny implementace konečných automatů používaných Hyperscanem. Různé způsoby zpomalení vyhledávačů regulárních výrazů jsou zhodnoceny a je zvolena metoda, která je založena na fungování jedné z implementací konečných automatů používaných v Hyperscanu. Na základě zvolené metody je implementován generátor, který pro vybraný výraz vygeneruje text, jehož skenování by mělo Hyperscanu zabrat výrazně déle než u normálního textu. Provedené benchmarky ukázaly, že pro některé regulární výrazy způsobil generovaný text v porovnání vůči náhodnému textu výrazné prodloužení vyhledávání Hyperscanem. U nejvíce ovlivněného regulárního výrazu trvalo skenování generovaného textu více než 8000krát déle než skenování náhodného textu.
|
|
|
Synthesis of Probabilistic Programs with Rewards
Hranička, Vojtěch ; Síč, Juraj (referee) ; Češka, Milan (advisor)
This thesis pursues the synthesis of probabilistic programs with rewards. Probabilistic synthesis leads to the automatic proposal of a system which fulfills required specifications. In this thesis, I work with a form of synthesis where we have a sketch of a given system. This sketch includes unknown variables and the objective is to find a combination of configuration of given variables in order to have the final program meeting the specified requirements. Recently, new approaches considering a set of solutions as a family of Markov chain have appeared. One of these approaches is the usage of a new method combining counterexample-guided abstraction refinement and counterexample-guided inductive synthesis. This method exceeds other methods for synthesis of probabilistic programs with its efficiency. In this thesis, I concretely focus on extending this tool's specification language by adding a possibility of application of rewards and until properties. Thanks to these extensions it is possible to specify searched solution more efficiently. Experiments demonstrate that even after the addition of these possibilities of specifications the speed of a given tool remains by a margin of order of magnitudes more effective than the standard method of synthesis.
|
|
|
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.
|
|
|
Simulation for Symbolic Automata
Síč, Juraj ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Symbolic automata are similar to classical automata with one big difference: transitions are labelled with predicates defined in separate logical theory. This allows usage of large alphabets while taking less space. In this work we are interested in computing simulation (a binary relation on states that language inclusion) for these automata. This can be then used for reducing the size of automata without the need to determinize them first. There exist few algorithms for computing simulation over Kripke structures, which were then altered to work over labeled transition systems and classical automata. We show how one of these algorithms can be modified for symbolic automata by using the partition of the alphabet domain that is compatible with the predicates labelling transitions and by using the possibilities of the alphabet theory.
|
|
|
Using Counter-Examples in Controller Synthesis for POMDPs
Frejlach, Jakub ; Síč, Juraj (referee) ; Češka, Milan (advisor)
Tato práce se zabývá částečně pozorovatelnými Markovskými rozhodovacími procesy \linebreak (POMDP), významnými stochastickými modely pro rozhodování za nejistoty a částečné pozorovatelnosti. POMDP lze aplikovat od navigace robotů až po samořídící vozidla. Nerozhodnutelný problém řízení POMDP vedl k různým přístupům, včetně konečných stavových kontrolerů (FSC) založených na pozorování a udržování histore v paměti. Identifikaci malých a ověřitelných FSC lze redukovat na syntézu Markovských řetězců. Tato práce se zaměřuje na induktivní syntézu řízenou protipříklady (CEGIS) implementovanou v rámci programu PAYNT a zkoumá využití Markovských rozhodovacích procesů jako protipříkladů. Je nastíněna nová hladová metoda pro konstrukci protipříkladů, která je implementována v programu PAYNT, která v některých případech vykazuje zlepšení oproti stávající metodě.
|
|
|
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.
|
|
|
Synthesis of Probabilistic Programs with Rewards
Hranička, Vojtěch ; Síč, Juraj (referee) ; Češka, Milan (advisor)
This thesis pursues the synthesis of probabilistic programs with rewards. Probabilistic synthesis leads to the automatic proposal of a system which fulfills required specifications. In this thesis, I work with a form of synthesis where we have a sketch of a given system. This sketch includes unknown variables and the objective is to find a combination of configuration of given variables in order to have the final program meeting the specified requirements. Recently, new approaches considering a set of solutions as a family of Markov chain have appeared. One of these approaches is the usage of a new method combining counterexample-guided abstraction refinement and counterexample-guided inductive synthesis. This method exceeds other methods for synthesis of probabilistic programs with its efficiency. In this thesis, I concretely focus on extending this tool's specification language by adding a possibility of application of rewards and until properties. Thanks to these extensions it is possible to specify searched solution more efficiently. Experiments demonstrate that even after the addition of these possibilities of specifications the speed of a given tool remains by a margin of order of magnitudes more effective than the standard method of synthesis.
|
|
|
Simulation for Symbolic Automata
Síč, Juraj ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Symbolic automata are similar to classical automata with one big difference: transitions are labelled with predicates defined in separate logical theory. This allows usage of large alphabets while taking less space. In this work we are interested in computing simulation (a binary relation on states that language inclusion) for these automata. This can be then used for reducing the size of automata without the need to determinize them first. There exist few algorithms for computing simulation over Kripke structures, which were then altered to work over labeled transition systems and classical automata. We show how one of these algorithms can be modified for symbolic automata by using the partition of the alphabet domain that is compatible with the predicates labelling transitions and by using the possibilities of the alphabet theory.
|
guest ::
