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.

我们提出了一种新技术，通过使用给定模型的 PRISM 程序构建一些模型的小版本并训练一个分类器，然后应用机器学习分类技术来近似相关分区，将分区结果作为标准双模拟技术的初始分区，以减少方法的运行时间。实验结果表明，该方法与最先进的工具相比，可以显著减少运行时间。