ASHOK, Pranav, Tomáš BRÁZDIL, Jan KŘETÍNSKÝ and 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, p. 322-335. ISBN 978-3-030-03420-7. Available from: https://dx.doi.org/10.1007/978-3-030-03421-4_21.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes
Authors ASHOK, Pranav (356 India), Tomáš BRÁZDIL (203 Czech Republic, belonging to the institution), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution) and Ondřej SLÁMEČKA (203 Czech Republic, belonging to the institution).
Edition Cham, Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), p. 322-335, 14 pp. 2018.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/18:00108292
Organization unit Faculty of Informatics
ISBN 978-3-030-03420-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-03421-4_21
Keywords in English Monte Carlo Tree Search; Reachability; Markov Decision Processes
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2020 07:54.
Abstract
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.
Links
GA18-11193S, research and development projectName: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy
Investor: Czech Science Foundation
PrintDisplayed: 1/8/2024 12:22