Monte Carlo Tree Search for Verifying Reachability in Markov
Decision Processes

D 2018

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

ASHOK, Pranav, Tomáš BRÁZDIL, Jan KŘETÍNSKÝ a Ondřej SLÁMEČKA

Základní údaje

Originální název

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

Autoři

ASHOK, Pranav (356 Indie), Tomáš BRÁZDIL (203 Česká republika, domácí), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí) a Ondřej SLÁMEČKA (203 Česká republika, domácí)

Vydání

Cham, Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), od s. 322-335, 14 s. 2018

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00108292

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-03420-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-03421-4_21

Klíčová slova anglicky

Monte Carlo Tree Search; Reachability; Markov Decision Processes

Změněno: 28. 4. 2020 07:54, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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ávaznosti

GA18-11193S, projekt VaV

Název: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Investor: Grantová agentura ČR, Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Citovat

ASHOK, Pranav, Tomáš BRÁZDIL, Jan KŘETÍNSKÝ a Ondřej SLÁMEČKA. Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. In Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). Cham: Springer, 2018, s. 322-335. ISBN 978-3-030-03420-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-03421-4_21.

@inproceedings{1649045,
   author = {Ashok, Pranav and Brázdil, Tomáš and Křetínský, Jan and Slámečka, Ondřej},
   address = {Cham},
   booktitle = {Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)},
   doi = {http://dx.doi.org/10.1007/978-3-030-03421-4_21},
   keywords = {Monte Carlo Tree Search; Reachability; Markov Decision Processes},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-03420-7},
   pages = {322-335},
   publisher = {Springer},
   title = {Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes},
   year = {2018}
}

TY  - JOUR
ID  - 1649045
AU  - Ashok, Pranav - Brázdil, Tomáš - Křetínský, Jan - Slámečka, Ondřej
PY  - 2018
TI  - Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes
PB  - Springer
CY  - Cham
SN  - 9783030034207
KW  - Monte Carlo Tree Search
KW  - Reachability
KW  - Markov Decision Processes
N2  - 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.
ER  -

ASHOK, Pranav, Tomáš BRÁZDIL, Jan KŘETÍNSKÝ a Ondřej SLÁMEČKA. Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. In \textit{Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)}. Cham: Springer, 2018, s.~322-335. ISBN~978-3-030-03420-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-03421-4\_{}21.

Podrobný výpis o publikaci