The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models?

Abstract. This paper presents a library for exactly computing the bisim-ilarity Kantorovich-based pseudometrics between Markov chains and be-tween Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are com-puted by using an on-the-fly greedy strategy that prevents the exhaustive state space exploration and does not require a complete storage of the data structures. Tests performed on a consistent set of (pseudo)randomly generated instances show that our algorithm improves the efficiency of the previously proposed iterative algorithms, on average, with orders of magnitude. The tool is available as a Mathematica package library.