TY - GEN
T1 - Monte carlo tree search for verifying reachability in markov decision processes
AU - Ashok, Pranav
AU - Brázdil, Tomáš
AU - Křetínský, Jan
AU - Slámečka, Ondřej
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018
Y1 - 2018
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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85056448503&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-03421-4_21
DO - 10.1007/978-3-030-03421-4_21
M3 - Conference contribution
AN - SCOPUS:85056448503
SN - 9783030034207
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 322
EP - 335
BT - Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Verlag
T2 - 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018
Y2 - 5 November 2018 through 9 November 2018
ER -