Title: Efficient Data Structures and Sorting Algorithms for Bisimulation

Speaker: David N. Jansen (Radboud Universiteit, The Netherlands)

        www.cs.ru.nl/D.Jansen

Time: 6th November 2014, 10:30

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

Markov chains are a well-known formalism widely used to model systems exhibiting probabilistic behavior. When working with Markov chains, we have to take care of the size of the state space that can quickly become difficult to manage, for instance when we are model checking properties of the Markov chain. A technique we can use to reduce this size of the original Markov chain is based on the computation of the smallest Markov chain that is behaviorally equivalent, or bisimilar, to the original one, where two states in a Markov chain are bisimilar if they essentially have the same transitions. By collapsing all bisimilar states into a single state, we can reduce greatly the number of states and consequently the essentially repeated computation steps we would perform on the original Markov chain. In this talk we explain how bisimulation minimisation can be done efficiently in time and space.