|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
|
|
Improving Synthesis of Finite State Controllers for POMDPs Using Belief Space Approximation
Macák, Filip ; Holík, Lukáš (referee) ; Češka, Milan (advisor)
Táto práca sa zameriava na kombináciu dvoch moderných metód syntézy plánovačov pre Markovské procesy s čiastočným pozorovaním (POMDPs), ktoré sú významným modelom pre sekvenčné rozhodovanie s neistotou. Hlavnou úlohou je nájsť plánovač POMDP, ktorý dosahuje čo najlepšiu hodnotu. Keďže hľadanie optimálneho plánovača je nerozhodnuteľné, zameriavame sa na syntézu dobrých konečne stavových kontrolérov (FSCs). V tejto práci integrujeme dve moderné, ortogonálne metódy pre syntézu kontrolérov POMDP, a to metódu založenú na prehľadávaní belief priestoru a induktívnu metódu. Prvá metóda získava FSC z konečného fragmentu takzvaného belief MDP, čo je MDP, ktorý udržiava prehľad o pravdepodobnostiach rovnako pozorovateľných stavov POMDP. Druhá je induktívna vyhľadávacia technika pre množinu FSC s fixnou veľkosťou pamäti. Kľúčovým výsledkom tejto práce je symbiotický algoritmus, ktorý integruje obidva tieto prístupy tak, aby sa každý dokázal zlepšiť z kontrolérov vytvorených tým druhým. Experimentálne výsledky naznačujú významné zlepšenie hodnoty kontrolérov pri značnom znižovaní času syntézy a využitej pamäte.
|
|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
|
|
Avoiding overfitting of models: an application to research data on the Internet videos
Jiroušek, Radim ; Krejčová, I.
The problem of overfitting is studied from the perspective of information theory. In this context, data-based model learning can be viewed as a transformation process, a process transforming the information contained in data into the information represented by a model. The overfitting of a model often occurs when one considers an unnecessarily complex model, which usually means that the considered model contains more information than the original data. Thus, using one of the basic laws of information theory saying that any transformation cannot increase the amount of information, we get the basic restriction laid on models constructed from data: A model is acceptable if it does not contain more information than the input data file.
|
|
| |
|
| |
|
|
Thoughts on belief and model revision with uncertain evidence
Vomlel, Jiří
Bayesian networks and other graphical probabilistic models became a popular framework for reasoning with uncertainty. Efficient methods have been developed for revising beliefs with new evidence. However, when the evidence is uncertain, i.e. represented by a probability distribution, different methods have been proposed. In this paper we analyze and compare these methods. The goal is to show in what cases they can be used correctly.
|
guest ::
