Improving Probabilistic Bisimulation for MDPs Using Machine Learning

TL;DR

This paper introduces a machine learning-based approach to improve probabilistic bisimulation for Markov Decision Processes, significantly reducing computation time by training classifiers on simplified models to initialize the bisimulation process.

Contribution

The paper presents a novel machine learning technique that accelerates probabilistic bisimulation by using classifiers trained on reduced models to initialize the partitioning process.

Findings

Significant reduction in bisimulation computation time.

Effective use of machine learning to approximate state partitions.

Improved efficiency over existing bisimulation algorithms.

Abstract

The utilization of model checking has been suggested as a formal verification technique for analyzing critical systems. However, the primary challenge in applying to complex systems is state space explosion problem. To address this issue, bisimulation minimization has emerged as a prominent method for reducing the number of states in a labeled transition system, aiming to overcome the difficulties associated with the state space explosion problem. In the case of systems exhibiting stochastic behaviors, probabilistic bisimulation is employed to minimize a given model, obtaining its equivalent form with fewer states. Recently, various techniques have been introduced to decrease the time complexity of the iterative methods used to compute probabilistic bisimulation for stochastic systems that display nondeterministic behaviors. In this paper, we propose a new technique to partition the state space of a given probabilistic model to its bisimulation classes. This technique uses the PRISM program of a given model and constructs some small versions of the model to train a classifier. It then applies machine learning classification techniques to approximate the related partition. The resulting partition is used as an initial one for the standard bisimulation technique in order to reduce the running time of the method. The experimental results show that the approach can decrease significantly the running time compared to state-of-the-art tools.