Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2018
Type Article in Proceedings
Conference Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-030-03421-4_21
Keywords Monte Carlo Tree Search; Reachability; Markov Decision Processes
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.