Verification of Markov Decision Processes using Learning Algorithms (2014)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/14:00075875 |
|---|---|
| Název v anglickém jazyce | Verification of Markov Decision Processes using Learning Algorithms |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2014 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 1 |
| Počet tvůrců celkem | 8 |
| Počet domácích tvůrců | 2 |
| Výčet všech uvedených jednotlivých tvůrců | Tomáš Brázdil (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1762834) Krishnendu Chatterjee (státní příslušnost: IN - Indická republika) Martin Chmelík (státní příslušnost: CZ - Česká republika, vedidk: 7692005) Vojtěch Forejt (státní příslušnost: CZ - Česká republika, vedidk: 2477912) Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054) Marta Kwiatkowska (státní příslušnost: PL - Polská republika) David Parker (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska) Mateusz Ujma (státní příslušnost: PL - Polská republika) |
| Popis výsledku v anglickém jazyce | We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Ourframework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties in MDPs. |
| Klíčová slova oddělená středníkem | stochastic systems; verification; machine learning; statistical model checking; reinforcement learning |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1007/978-3-319-11936-6_8 |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014 |
|---|---|
| ISBN | 9783319119359 |
| ISSN | 0302-9743 |
| Počet stran výsledku | 17 |
| Strana od-do | 98-114 |
| Název nakladatele | Springer |
| Místo vydání | Heidelberg Dordrecht London New York |
| Místo konání akce | Heidelberg Dordrecht London New York |
| Datum konání akce | 2014 |
| Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2015 |
| Specifikace | RIV/00216224:14330/14:00075875!RIV15-MSM-14330___ |
| Datum poslední aktualizace výsledku | 29.05.2015 |
| Kontrolní číslo | 152393877 |
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Podpora / návaznosti | Specifický výzkum na vysokých školách, poskytovatel MŠMT |
|---|