Explainability is a Game for Probabilistic Bisimilarity Distances

Abstract

Software bugs cost trillions annually, requiring better bug detection tools. Testing is widely used but has limitations, especially in non-deterministic software, where code produces different outputs even with fixed inputs due to randomness and concurrency. Labelled Markov chains model randomness but suffer from state space explosion problem, where the number of states grows exponentially with system complexity. One solution is to identify behaviorally equivalent states using probabilistic bisimilarity. However, this method is not robust, small changes in probabilities can affect equivalences. To address this, probabilistic bisimilarity distances were introduced, a quantitative generalization of probabilistic bisimilarity. These distances have game-theoretic characterizations. This thesis illustrates how optimal policies, known as player's strategies, can explain distances. We formulate 1-maximal and 0-minimal policies, argue that they lead to better explanations. We present algorithms for these policies, prove an exponential lower bound for the 1-maximal algorithm, and show that symmetries simplify policies and, hence, explanations.