|
|
Heuristics in String Solving
Řezáč, Michal ; Havlena, Vojtěch (oponent) ; Síč, Juraj (vedoucí práce)
This work aims on identifying heuristics and strategies used in modern string solvers and evaluating their impact on the effectiveness of the solving. In particular, two solvers -- cvc5 and Z3 -- are examined. The thesis describes the techniques used by SMT solvers and the strategies implemented by string solvers. The evaluation of the effectiveness of the heuristics was performed by disabling them directly in the code of the tools mentioned and then evaluating the impact on solving the sets of standard benchmarks. The result of this work is summary of a set of specific heuristics and a description of the structure of the tools cvc5 and Z3. The measurements failed to demonstrate the actual impact of the heuristics identified and described.
|
|
|
Finding Weaknesses of Hyperscan
Hrabovský, Jiří ; Vojnar, Tomáš (oponent) ; Síč, Juraj (vedoucí práce)
This Bachelor's thesis aims to explain how the open sourced regular expression matcher Hyperscan works, and provide overview of algorithms it uses internally. The second objective is conducting experiments to determine how much can the performance of the matcher be affected by the scanned text. Based on the source code and articles by the authors of Hyperscan the overview of how Hyperscan scans the text for patterns is provided in chapter 3 and the implementations of NFA (Nondeterministic Finite Automata) used by the Hyperscaned are explained in chapter 4. How could the matcher be slowed down by input text is discussed and approach focusing on specific implementation of NFA used by Hyperscan is proposed. Generator using the proposed approach that is able to generate text for some expressions, that when scanned using Hyperscan with the given expression takes significantly longer that normal text. Conducted benchmark showed that for some expressions the generated text caused the Hyperscan to scan significantly longer. The most affected regular expression took more than 8000 times longer when scanning the generated text than the random text.
|
|
|
Syntéza pravděpodobnostních programů s optimální cenou
Hranička, Vojtěch ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá syntézou pravděpodobnostních modelů s optimální cenou. Pravděpodobnostní syntéza slouží k automatickému návrhu systému, který splňuje požadované specifikace. V této práci se věnuji způsobu syntézy kde máme šablonu pro daný systém, která obsahuje neznámé části a cílem je najít takovou kombinaci nastavení daných částí tak, aby výsledný systém splňoval specifikované požadavky. V poslední době se objevují nové přístupy uvažující o množině řešení jako o rodině Markovových řetězců. Jedním z těchto přístupů je použití nové metody kombinující metody protipříklady řízeného zjemňování abstrakce a induktivní syntézy. Tato metoda svou efektivitou převyšuje ostatní metody pro pravděpodobnostní syntézu. V této práci se konkrétně zaměřuji na rozšíření specifikačního jazyka tohoto nástroje o možnost použití takzvaných rewardů a until vlastností. Díky těmto rozšířením je možné lépe a jednodušeji specifikovat hledané řešení. Experimenty demonstrují, že i po rozšíření daného nástroje o tyto možnosti specifikace jeho rychlost v porovnání se standardní metodou syntézy zůstává až o několik řádů efektivnější.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (oponent) ; Holík, Lukáš (vedoucí práce)
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.
|
|
|
Simulace pro symbolické automaty
Síč, Juraj ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
Symbolické automaty sú podobné klasickým automatom s jedným veľkým rozdielom: prechody sú značené predikátmi definovanými v oddelenej teórii. Toto umožňuje použiť veľké abecedy s pouźitím oveľa menšieho miesta. V tejto práci sa zaoberáme výpočtom simulácie (binárnej relácie nad množinou stavov, ktorá aproximuje jazykovú inklúziu) pre tieto automaty. Táto relácia sa dá potom použiť pri redukovaní počtu stavov bez nutnosti determinizácie. Existuje niekoľko algoritomv pre výpočet simulácie pre Kripkeho štruktúry, ktoré boli neskôr modifikované pre označené prechodové systémy a klasické automaty. V tejto práci ukážeme ako sa dá jeden z týchto algoritmov modifikovať pre symbolické automaty použitím rozkladu domény abecedy ktorý je kompatibilný s predikátmi značiacimi prechody a použitím možností teórie abecedy.
|
|
|
Using Counter-Examples in Controller Synthesis for POMDPs
Frejlach, Jakub ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
This thesis examines partially observable Markov decision processes (POMDPs), a prominent stochastic model for decision-making under uncertainty and partial observability. POMDPs have diverse applications, from robot navigation to self-driving vehicles. The undecidable control problem of POMDPs has led to various approaches, including finite-state controllers (FSCs) based on observations and history. Identifying small and verifiable FSCs reduces the synthesis of Markov chains. This thesis focuses on counterexample-guided inductive synthesis (CEGIS) within the PAYNT program, exploring the use of Markov decision processes as counterexamples. A new greedy method for constructing counterexamples is outlined and implemented in PAYNT, showing improvements in some cases compared to the existing method.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (oponent) ; Holík, Lukáš (vedoucí práce)
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.
|
|
|
Syntéza pravděpodobnostních programů s optimální cenou
Hranička, Vojtěch ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá syntézou pravděpodobnostních modelů s optimální cenou. Pravděpodobnostní syntéza slouží k automatickému návrhu systému, který splňuje požadované specifikace. V této práci se věnuji způsobu syntézy kde máme šablonu pro daný systém, která obsahuje neznámé části a cílem je najít takovou kombinaci nastavení daných částí tak, aby výsledný systém splňoval specifikované požadavky. V poslední době se objevují nové přístupy uvažující o množině řešení jako o rodině Markovových řetězců. Jedním z těchto přístupů je použití nové metody kombinující metody protipříklady řízeného zjemňování abstrakce a induktivní syntézy. Tato metoda svou efektivitou převyšuje ostatní metody pro pravděpodobnostní syntézu. V této práci se konkrétně zaměřuji na rozšíření specifikačního jazyka tohoto nástroje o možnost použití takzvaných rewardů a until vlastností. Díky těmto rozšířením je možné lépe a jednodušeji specifikovat hledané řešení. Experimenty demonstrují, že i po rozšíření daného nástroje o tyto možnosti specifikace jeho rychlost v porovnání se standardní metodou syntézy zůstává až o několik řádů efektivnější.
|
|
|
Simulace pro symbolické automaty
Síč, Juraj ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
Symbolické automaty sú podobné klasickým automatom s jedným veľkým rozdielom: prechody sú značené predikátmi definovanými v oddelenej teórii. Toto umožňuje použiť veľké abecedy s pouźitím oveľa menšieho miesta. V tejto práci sa zaoberáme výpočtom simulácie (binárnej relácie nad množinou stavov, ktorá aproximuje jazykovú inklúziu) pre tieto automaty. Táto relácia sa dá potom použiť pri redukovaní počtu stavov bez nutnosti determinizácie. Existuje niekoľko algoritomv pre výpočet simulácie pre Kripkeho štruktúry, ktoré boli neskôr modifikované pre označené prechodové systémy a klasické automaty. V tejto práci ukážeme ako sa dá jeden z týchto algoritmov modifikovať pre symbolické automaty použitím rozkladu domény abecedy ktorý je kompatibilný s predikátmi značiacimi prechody a použitím možností teórie abecedy.
|
host ::
