Improving Probabilistic Bisimulation for MDPs Using Machine Learning

‎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 the state space explosion problem‎. ‎To address this issue‎, ‎bisimulation minimization has emerged as a prominent method for reducing the number of states in a system‎, ‎aiming to overcome the difficulties associated with the state space explosion problem‎. ‎For systems with stochastic behaviors‎, ‎probabilistic bisimulation is employed to minimize a given model‎, ‎obtaining its equivalent form with fewer states‎. ‎In this paper‎, ‎we propose a novel 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 supervised machine learning techniques to approximately classify the related partition‎. ‎The resulting partition is then used to accelerate the standard bisimulation technique‎, ‎significantly reducing 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‎.