|
|
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ů.
|
|
|
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ší.
|
|
|
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.
|
|
|
Generování protipříkladů při analýze Markovových modelů
Molek, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá generováním protipříkladů v kontextu verifikace pravděpodobnostních systémů. Protipříklady jsou generovány nad Markovovými modely (přesněji DTMC). Specifikace vlastností modelu jsou zadávány pomocí logiky PCTL, která je v této práci popsána. Pro generování protipříkladů byly použity dva různé algoritmy (Best-first search a Recursive Enumration Algorithm). Práce obsahuje popis implementace algoritmů do verifikačního nástroje STORM. Výsledky experimentů ukazují, že REA je schopen pracovat s modely obsahující miliony stavů.
|
|
|
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ší.
|
|
|
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.
|
|
|
Generování protipříkladů při analýze Markovových modelů
Molek, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá generováním protipříkladů v kontextu verifikace pravděpodobnostních systémů. Protipříklady jsou generovány nad Markovovými modely (přesněji DTMC). Specifikace vlastností modelu jsou zadávány pomocí logiky PCTL, která je v této práci popsána. Pro generování protipříkladů byly použity dva různé algoritmy (Best-first search a Recursive Enumration Algorithm). Práce obsahuje popis implementace algoritmů do verifikačního nástroje STORM. Výsledky experimentů ukazují, že REA je schopen pracovat s modely obsahující miliony stavů.
|
|
|
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.