Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes

Pranav Ashok, Tomáš Brázdil, Jan Křetínský +1

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 intr…