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‎.