|
|
Aproximativní techniky pro Markovovy modely
Andriushchenko, Roman ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Předkládaná práce je zaměřena na popis aproximativních technik pro analýzu Markovských řetězců, konkrétně na metody založené na agregaci nebo ořezávání stavového prostoru. Na začátku je představen postup umožňující aplikaci agregace pro modely diskrétního času s libovolnou strukturou stavového prostoru a je odvozen lepší odhad aproximační chyby. Daný postup je pak propojen s uniformizačními technikami, jak se standardní tak s adaptivní, což umožňuje provádět analýzu řetězců spojitého času spolu s odhadem aproximační chyby. Navržená technika spolu s existujícími metodami založenými na ořezávání byly implementovány v rámci nástroje PRISM. Provedené experimenty potvrzuji, že nově odvozený odhad aproximační chyby vylepšuje přesnost o několik řádů bez zhoršení celkové výkonnosti. Je ukázano, že výsledná agregační metoda je schopna poskytnout validní aproximaci modelu spolu s adekvátními odhady aproximační chyby, a to jak v diskrétním tak i ve spojitém čase. Následně je provedeno porovnání s technikami založenými na ořezávání stavového prostoru a je diskutováno pro které třídy Markovských řetězců je ta či ona metoda použitelnější. Nakonec je demonstrováno úspěšne použití aproximativních technik pro model checking Markovových modelů.
|
|
|
Computer-Aided Synthesis of Probabilistic Models
Andriushchenko, Roman ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
This thesis considers the problem of automated synthesis of probabilistic systems: having a family of Markov chains, how can one efficiently identify a chain satisfying a given specification? Such families often arise in various domains of engineering when modeling systems under uncertainty, and deciding even the simplest problems shows to be NP-hard. To tackle this problem, we adopt the principles of counterexample-guided inductive synthesis (CEGIS) and abstraction refinement (CEGAR) and develop a novel integrated technique for probabilistic synthesis. Experiments on practically relevant case studies demonstrate that the designed technique is not only comparable to state-of-the-art synthesis approaches, in most cases it manages to significantly outperform existing methods, sometimes by a margin of orders of magnitude.
|
|
|
Novel Methods for Semi-Quantitative Analysis of Biochemical Systems
Bíl, Jan ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
This thesis aims on providing novel methods for analysis of stochastic bio-chemical systems. It introduces a new population abstraction based on dirac semi-Markov processes. It turned out, that this abstraction is more precise than Continuous time Markov chain abstraction. On this abstraction, analysis methods are provided. Algorithm for transient analysis over this abstraction is described and also novel timed temporal logic formulas, that allow to express interesting biological properties are presented. Further, model-checking algorithm for these formulas is proposed and implemented. Preliminary experiments showing potential of this approach are also described.
|
|
|
GPU akcelerace grafových algoritmů
Lorenc, David ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
V této bakalářské práci se budu zabývat akcelerací algoritmu BFS (Breadth-first search) na grafické kartě. Jedná se algoritmus určený k průchodu grafem do šířky. Vysvětlím základní techniky paralelizace rozdělené podle Flynnovy klasifikace. Dále se budu zabývat stávajícími metodami paralelizace BFS na GPU. Následně provedu strukturované experimenty všech přístupů na stejném datasetu, porovnám a zhodnotím výsledky. Pro někoho nového je velice těžké se zorientovat v té to oblasti, z důvodu rozsáhlosti, chtěl jsem vytvořit práci která provede programátora začínajícího s paralelizací na GPU a umožní mu tak snazší vhled do této problematiky. Dále jsem se zaměřil na strukturované testování jednotlivých přístupů z různých prací a zhodnotil je z důvodu přehledu výkonosti přístupů na jednom místě. Čtenář tedy může vidět, který z nich je nejvhodnější pro jeho potřebu. Srozumitelné vysvětlení teorie týkající se technik a problémů paralelizace, popis hardwarového a softwarového konceptu NVDIA Cuda. Představení možností reprezentace grafů v paměti a vysvětlení proč se používá reprezentace grafu za pomocí listu sousednosti. Popis jednotlivých přístupů a jejich testování, na základě výsledků zhodnocení efektivity přístupů.
|
|
|
Reinforcement Learning for Automated Stock Portfolio Allocation
Lapeš, Zdeněk ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
This thesis is focused on the topic of reinforcement learning applied to a task of portfolio allocation. To accomplish this objective, the thesis first presents an overview of the fundamental theory, which includes the latest value-based and policy-based methods. Following that, the thesis describes the Stock portfolio environment, and finally, the experimental and implementation details are presented. The creation of datasets is discussed in detail, along with the rationale and methodology behind it. The RL agent is then trained and tested on three datasets, and the results obtained are promising and outperform common benchmarks. However, it was discovered that the annual return of the agent is still not better than the returns generated by the world’s top investors. The pipeline was implemented in Python 3.10, and technology from Weights & Biases was used to monitor all datasets, models, and hyperparameters. In conclusion, this work represents a significant step forward in the development of more effective RL agents for financial investments, with the potential to exceed even the performance of the world’s greatest investors.
|
|
|
Novel Methods for Semi-Quantitative Analysis of Biochemical Systems
Bíl, Jan ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
This thesis aims on providing novel methods for analysis of stochastic bio-chemical systems. It introduces a new population abstraction based on dirac semi-Markov processes. It turned out, that this abstraction is more precise than Continuous time Markov chain abstraction. On this abstraction, analysis methods are provided. Algorithm for transient analysis over this abstraction is described and also novel timed temporal logic formulas, that allow to express interesting biological properties are presented. Further, model-checking algorithm for these formulas is proposed and implemented. Preliminary experiments showing potential of this approach are also described.
|
|
|
Computer-Aided Synthesis of Probabilistic Models
Andriushchenko, Roman ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
This thesis considers the problem of automated synthesis of probabilistic systems: having a family of Markov chains, how can one efficiently identify a chain satisfying a given specification? Such families often arise in various domains of engineering when modeling systems under uncertainty, and deciding even the simplest problems shows to be NP-hard. To tackle this problem, we adopt the principles of counterexample-guided inductive synthesis (CEGIS) and abstraction refinement (CEGAR) and develop a novel integrated technique for probabilistic synthesis. Experiments on practically relevant case studies demonstrate that the designed technique is not only comparable to state-of-the-art synthesis approaches, in most cases it manages to significantly outperform existing methods, sometimes by a margin of orders of magnitude.
|
|
|
Aproximativní techniky pro Markovovy modely
Andriushchenko, Roman ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Předkládaná práce je zaměřena na popis aproximativních technik pro analýzu Markovských řetězců, konkrétně na metody založené na agregaci nebo ořezávání stavového prostoru. Na začátku je představen postup umožňující aplikaci agregace pro modely diskrétního času s libovolnou strukturou stavového prostoru a je odvozen lepší odhad aproximační chyby. Daný postup je pak propojen s uniformizačními technikami, jak se standardní tak s adaptivní, což umožňuje provádět analýzu řetězců spojitého času spolu s odhadem aproximační chyby. Navržená technika spolu s existujícími metodami založenými na ořezávání byly implementovány v rámci nástroje PRISM. Provedené experimenty potvrzuji, že nově odvozený odhad aproximační chyby vylepšuje přesnost o několik řádů bez zhoršení celkové výkonnosti. Je ukázano, že výsledná agregační metoda je schopna poskytnout validní aproximaci modelu spolu s adekvátními odhady aproximační chyby, a to jak v diskrétním tak i ve spojitém čase. Následně je provedeno porovnání s technikami založenými na ořezávání stavového prostoru a je diskutováno pro které třídy Markovských řetězců je ta či ona metoda použitelnější. Nakonec je demonstrováno úspěšne použití aproximativních technik pro model checking Markovových modelů.
|
host ::
RSS.