Bisimulation(s) and Probabilistic Model Checking

 

Varun Aggarwala

 

 

Abstract:

Bisimulation is an important method for state space reduction in case of
Model Checking. It exploits the structure of the markovian model to have
significant state space reductions. As for the case of bisimulation over
ordinary model checking we still have state space reduction but time
constraints makes that practically ineffective. However the picture
changes in the case of Probabilistic Model Checking where we also have
time reduction along with state space reduction making it a sought-after
technique.

In the talk we would like to discuss the strong bisimulation algorithm and
compare the time taken by it using different efficient binary tree
implementations like splay or red black tree. Also weak bisimulation and
backward bisimulation will be discussed and how they can be used to reduce
the state space. Their advantages and limitations and comparison with
strong bisimulation will also be discussed.