  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.
