Improving Probabilistic Bisimulation for MDPs Using Machine Learning
Mohammadsadegh Mohaghegh Khayyam Salehi
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.