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程序，构建该模型的若干小型版本以训练分类器，随后应用机器学习分类技术来近似相关划分。所得划分被用作标准互模拟技术的初始划分，以降低该方法运行时间。实验结果表明，与现有先进工具相比，该方法能显著降低运行时间。