The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models
This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are computed 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.
KeywordsDiscount Factor Markov Decision Process Probability Transition Matrix Greedy Strategy Action Label
Unable to display preview. Download preview PDF.
- 1.Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Computing behavioral distances, compositionally. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 74–85. Springer, Heidelberg (2013)Google Scholar
- 5.Ferns, N., Panangaden, P., Precup, D.: Metrics for finite Markov Decision Processes. In: Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence, UAI, pp. 162–169. AUAI Press (2004)Google Scholar
- 8.van Breugel, F., Sharma, B., Worrell, J.: Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems. Logical Methods in Computer Science 4(2), 1–23 (2008)Google Scholar