On Probabilistic Bisimilarity Distances of Labelled Markov Chains

In the realm of model checking, labelled Markov chains are commonly
used to model systems that exhibit random behaviour. Probabilistic bisimilarity is a
technique used to minimize the state space of a labelled Markov chain in order to
combat state space explosion. In this talk, we will discuss probabilistic bisimilarity
distances, a quantitative generalization of probabilistic bisimilarity. It is a
pseudometric that assigns real-value distances to pairs of states, which captures
the similarity of their behaviour. Through some examples, we will also show that
these distances can depend discontinuously on the transition probabilities, leading
to unexpected behaviour changes.