Verification of Markov Decision Processes using Learning Algorithms

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00075875" target="_blank" >RIV/00216224:14330/14:00075875 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_8" target="_blank" >http://dx.doi.org/10.1007/978-3-319-11936-6_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_8" target="_blank" >10.1007/978-3-319-11936-6_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of Markov Decision Processes using Learning Algorithms

Popis výsledku v původní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.

Název v anglickém jazyce

Verification of Markov Decision Processes using Learning Algorithms

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014

ISBN

9783319119359

ISSN

0302-9743

e-ISSN

—

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

1. 1. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—