Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00108292" target="_blank" >RIV/00216224:14330/18:00108292 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-03421-4_21" target="_blank" >http://dx.doi.org/10.1007/978-3-030-03421-4_21</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-03421-4_21" target="_blank" >10.1007/978-3-030-03421-4_21</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

Popis výsledku v původním jazyce

The maximum reachability probabilities in a Markov decision process can be computed using value iteration (VI). Recently, simulation-based heuristic extensions of VI have been introduced, such as bounded real-time dynamic programming (BRTDP), which often manage to avoid explicit analysis of the whole state space while preserving guarantees on the computed result. In this paper, we introduce a new class of such heuristics, based on Monte Carlo tree search (MCTS), a technique celebrated in various machine-learning settings. We provide a spectrum of algorithms ranging from MCTS to BRTDP. We evaluate these techniques and show that for larger examples, where VI is no more applicable, our techniques are more broadly applicable than BRTDP with only a minor additional overhead.

Název v anglickém jazyce

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

Popis výsledku anglicky

The maximum reachability probabilities in a Markov decision process can be computed using value iteration (VI). Recently, simulation-based heuristic extensions of VI have been introduced, such as bounded real-time dynamic programming (BRTDP), which often manage to avoid explicit analysis of the whole state space while preserving guarantees on the computed result. In this paper, we introduce a new class of such heuristics, based on Monte Carlo tree search (MCTS), a technique celebrated in various machine-learning settings. We provide a spectrum of algorithms ranging from MCTS to BRTDP. We evaluate these techniques and show that for larger examples, where VI is no more applicable, our techniques are more broadly applicable than BRTDP with only a minor additional overhead.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA18-11193S" target="_blank" >GA18-11193S: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2018

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

Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)

ISBN

9783030034207

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

14

Strana od-do

322-335

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Cham

Datum konání akce

1. 1. 2018

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

CST - Celostátní akce

Kód UT WoS článku

—