Model checking has been proposed as a formal verification approach for analyzing computer-based and cyber-physical systems. The state space explosion problem is the main obstacle for applying this approach for sophisticated systems. Bisimulation minimization is a prominent method for reducing the number of states in a labeled transition system and is used to alleviate the challenges of the state space explosion problem. For systems with stochastic behaviors, probabilistic bisimulation is used to reduce a given model to its minimized equivalent one. In recent years, several techniques have been proposed to reduce the time complexity of the iterative methods for computing probabilistic bisimulation of stochastic systems with nondeterministic behaviors. In this paper, we propose several techniques to accelerate iterative processes to partition the state space of a given probabilistic model to its bisimulation classes. The first technique applies two ordering heuristics for choosing splitter blocks. The second technique uses hash tables to reduce the running time and the average time complexity of the standard iterative method. The proposed approaches are implemented and run on several conventional case studies and reduce the running time by one order of magnitude on average.

翻译：模型检测已被提出作为一种形式化验证方法，用于分析基于计算机的信息物理系统。状态空间爆炸问题是该方法应用于复杂系统的主要障碍。对分模拟最小化是减少标注转移系统中状态数量的重要方法，并用于缓解状态空间爆炸问题带来的挑战。对于具有随机行为的系统，采用概率对分模拟将给定模型约简为其最小化等价模型。近年来，已提出多种技术以降低计算具有非确定性行为的随机系统概率对分模拟的迭代方法的时间复杂度。本文提出了若干加速迭代过程的技术，用于将给定概率模型的状态空间划分为其对分类。第一项技术采用两种分割块排序启发式策略。第二项技术利用哈希表减少标准迭代方法的运行时间及平均时间复杂度。所提出的方法已在多个常规案例研究中实现并运行，平均运行时间降低了一个数量级。