Monte Carlo Tree
Search in Verification of Markov Decision Processes

During 2017 I researched how to use Monte Carlo Tree Search (a machine learning technique popularized mainly by its success in Go and Chess) to verify properties of Markov Decision Processes (in MDPs you can choose actions but there are probabilities influencing where the process goes, see zeroconf as an example).

This was a joint work with my advisor Tomáš Brázdil, Pranav Ashok, and Jan Křetínský. We have managed to come up with algorithms which outperform known approaches (e.g., value iteration or BRTDP) on some of the common benchmarks and we have shown there are models where our algorithms are significantly better. You can read the details in our paper published in the proceedings of ISoLA 2018.