Tags:Machine Learning, Probabilistic Model Checking and Qualitative Verification
Abstract:
State explosion is a well-known challenge of model checking. In this paper we propose several approaches to improve the standard techniques for verifying qualitative reachability properties of Markov decision Processes. For the first approach, we use two heuristics to reduce the total number of iterations of the standard iterative methods. The second approach uses the secondary hard disks for storing the information of a model and uses the main memory for a back-ward technique on the standard methods. The third approach uses a machine learning technique to classify the state space of a model to the related classes. While this approach does not need any memory overhead, its running times is much less than the running time of the standard approaches and can be used to cope the state explosion problem.
Machine Learning and Disk Based Methods for Qualitative Verification of Markov Decision Processes